(* 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
begin
subsection \<open>Pattern-match monad\<close>
default_sort cpo
pcpodef '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 \<open>Run operator\<close>
definition
run :: "'a match \ 'a::pcpo" where
"run = (\ m. sscase\\\(fup\ID)\(Rep_match m))"
text \<open>rewrite rules for run\<close>
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 \<open>Monad plus operator\<close>
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 \<open>rewrite rules for mplus\<close>
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 \<open>Match functions for built-in types\<close>
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 \<open>Mutual recursion\<close>
text \<open>
The following rules are used to prove unfolding theorems from
fixed-point definitions of mutually recursive functions.
\<close>
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 \<open>lemma for proving rewrite rules\<close>
lemma ssubst_lhs: "\t = s; P s = Q\ \ P t = Q"
by simp
subsection \<open>Initializing the fixrec package\<close>
ML_file \<open>Tools/holcf_library.ML\<close>
ML_file \<open>Tools/fixrec.ML\<close>
method_setup fixrec_simp = \<open>
Scan.succeed (SIMPLE_METHOD' o Fixrec.fixrec_simp_tac)
\<close> "pattern prover for fixrec constants"
setup \<open>
Fixrec.add_matchers
[ (\<^const_name>\<open>up\<close>, \<^const_name>\<open>match_up\<close>),
(\<^const_name>\<open>sinl\<close>, \<^const_name>\<open>match_sinl\<close>),
(\<^const_name>\<open>sinr\<close>, \<^const_name>\<open>match_sinr\<close>),
(\<^const_name>\<open>spair\<close>, \<^const_name>\<open>match_spair\<close>),
(\<^const_name>\<open>Pair\<close>, \<^const_name>\<open>match_Pair\<close>),
(\<^const_name>\<open>ONE\<close>, \<^const_name>\<open>match_ONE\<close>),
(\<^const_name>\<open>TT\<close>, \<^const_name>\<open>match_TT\<close>),
(\<^const_name>\<open>FF\<close>, \<^const_name>\<open>match_FF\<close>),
(\<^const_name>\<open>bottom\<close>, \<^const_name>\<open>match_bottom\<close>) ]
\<close>
hide_const (open) succeed fail run
end
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
