Quelle Fixrec.thy Sprache: Isabelle

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

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

section \<open>Fixed point operator and admissibility\<close>

subsection \<open>Iteration\<close>

primrec iterate :: "nat \ ('a \ 'a) \ ('a \ 'a)"
  where
    "iterate 0 = (\ F x. x)"
  | "iterate (Suc n) = (\ F x. F\(iterate n\F\x))"

text \<open>Derive inductive properties of iterate from primitive recursion\<close>

lemma iterate_0 [simp]: "iterate 0\F\x = x"
  by simp

lemma iterate_Suc [simp]: "iterate (Suc n)\F\x = F\(iterate n\F\x)"
  by simp

declare iterate.simps [simp del]

lemma iterate_Suc2: "iterate (Suc n)\F\x = iterate n\F\(F\x)"
  by (induct n) simp_all

lemma iterate_iterate: "iterate m\F\(iterate n\F\x) = iterate (m + n)\F\x"
  by (induct m) simp_all

text \<open>The sequence of function iterations is a chain.\<close>

lemma chain_iterate [simp]: "chain (\i. iterate i\F\\)"
  by (rule chainI, unfold iterate_Suc2, rule monofun_cfun_arg, rule minimal)

subsection \<open>Least fixed point operator\<close>

definition "fix" :: "('a::pcpo \ 'a) \ 'a"
  where "fix = (\ F. \i. iterate i\F\\)"

text \<open>Binder syntax for \<^term>\<open>fix\<close>\<close>

abbreviation fix_syn :: "('a::pcpo \ 'a) \ 'a" (binder \\ \ 10)
  where "fix_syn (\x. f x) \ fix\(\ x. f x)"

notation (ASCII)
  fix_syn  (binder \<open>FIX \<close> 10)

text \<open>Properties of \<^term>\<open>fix\<close>\<close>

text \<open>direct connection between \<^term>\<open>fix\<close> and iteration\<close>

lemma fix_def2: "fix\F = (\i. iterate i\F\\)"
  by (simp add: fix_def)

lemma iterate_below_fix: "iterate n\f\\ \ fix\f"
  unfolding fix_def2
  using chain_iterate by (rule is_ub_thelub)

text \<open>
  Kleene's fixed point theorems for continuous functions in pointed
  omega cpo's
\<close>

lemma fix_eq: "fix\F = F\(fix\F)"
  apply (simp add: fix_def2)
  apply (subst lub_range_shift [of _ 1, symmetric])
   apply (rule chain_iterate)
  apply (subst contlub_cfun_arg)
   apply (rule chain_iterate)
  apply simp
  done

lemma fix_least_below: "F\x \ x \ fix\F \ x"
  apply (simp add: fix_def2)
  apply (rule lub_below)
   apply (rule chain_iterate)
  apply (induct_tac i)
   apply simp
  apply simp
  apply (erule rev_below_trans)
  apply (erule monofun_cfun_arg)
  done

lemma fix_least: "F\x = x \ fix\F \ x"
  by (rule fix_least_below) simp

lemma fix_eqI:
  assumes fixed: "F\x = x"
    and least: "\z. F\z = z \ x \ z"
  shows "fix\F = x"
  apply (rule below_antisym)
   apply (rule fix_least [OF fixed])
  apply (rule least [OF fix_eq [symmetric]])
  done

lemma fix_eq2: "f \ fix\F \ f = F\f"
  by (simp add: fix_eq [symmetric])

lemma fix_eq3: "f \ fix\F \ f\x = F\f\x"
  by (erule fix_eq2 [THEN cfun_fun_cong])

lemma fix_eq4: "f = fix\F \ f = F\f"
  by (erule ssubst) (rule fix_eq)

lemma fix_eq5: "f = fix\F \ f\x = F\f\x"
  by (erule fix_eq4 [THEN cfun_fun_cong])

text \<open>strictness of \<^term>\<open>fix\<close>\<close>

lemma fix_bottom_iff: "fix\F = \ \ F\\ = \"
  apply (rule iffI)
   apply (erule subst)
   apply (rule fix_eq [symmetric])
  apply (erule fix_least [THEN bottomI])
  done

lemma fix_strict: "F\\ = \ \ fix\F = \"
  by (simp add: fix_bottom_iff)

lemma fix_defined: "F\\ \ \ \ fix\F \ \"
  by (simp add: fix_bottom_iff)

text \<open>\<^term>\<open>fix\<close> applied to identity and constant functions\<close>

lemma fix_id: "(\ x. x) = \"
  by (simp add: fix_strict)

lemma fix_const: "(\ x. c) = c"
  by (subst fix_eq) simp

subsection \<open>Fixed point induction\<close>

lemma fix_ind: "adm P \ P \ \ (\x. P x \ P (F\x)) \ P (fix\F)"
  unfolding fix_def2
  apply (erule admD)
   apply (rule chain_iterate)
  apply (rule nat_induct, simp_all)
  done

lemma cont_fix_ind: "cont F \ adm P \ P \ \ (\x. P x \ P (F x)) \ P (fix\(Abs_cfun F))"
  by (simp add: fix_ind)

lemma def_fix_ind: "\f \ fix\F; adm P; P \; \x. P x \ P (F\x)\ \ P f"
  by (simp add: fix_ind)

lemma fix_ind2:
  assumes adm: "adm P"
  assumes 0: "P \" and 1: "P (F\\)"
  assumes step: "\x. \P x; P (F\x)\ \ P (F\(F\x))"
  shows "P (fix\F)"
  unfolding fix_def2
  apply (rule admD [OF adm chain_iterate])
  apply (rule nat_less_induct)
  apply (case_tac n)
   apply (simp add: 0)
  apply (case_tac nat)
   apply (simp add: 1)
  apply (frule_tac x=nat in spec)
  apply (simp add: step)
  done

lemma parallel_fix_ind:
  assumes adm: "adm (\x. P (fst x) (snd x))"
  assumes base: "P \ \"
  assumes step: "\x y. P x y \ P (F\x) (G\y)"
  shows "P (fix\F) (fix\G)"
proof -
  from adm have adm': "adm (case_prod P)"
    unfolding split_def .
  have "P (iterate i\F\\) (iterate i\G\\)" for i
    by (induct i) (simp add: base, simp add: step)
  then have "\i. case_prod P (iterate i\F\\, iterate i\G\\)"
    by simp
  then have "case_prod P (\i. (iterate i\F\\, iterate i\G\\))"
    by - (rule admD [OF adm'], simp, assumption)
  then have "case_prod P (\i. iterate i\F\\, \i. iterate i\G\\)"
    by (simp add: lub_Pair)
  then have "P (\i. iterate i\F\\) (\i. iterate i\G\\)"
    by simp
  then show "P (fix\F) (fix\G)"
    by (simp add: fix_def2)
qed

lemma cont_parallel_fix_ind:
  assumes "cont F" and "cont G"
  assumes "adm (\x. P (fst x) (snd x))"
  assumes "P \ \"
  assumes "\x y. P x y \ P (F x) (G y)"
  shows "P (fix\(Abs_cfun F)) (fix\(Abs_cfun G))"
  by (rule parallel_fix_ind) (simp_all add: assms)

subsection \<open>Fixed-points on product types\<close>

text \<open>
  Bekic's Theorem: Simultaneous fixed points over pairs
  can be written in terms of separate fixed points.
\<close>

lemma fix_cprod:
  fixes F :: "'a::pcpo \ 'b::pcpo \ 'a \ 'b"
  shows
    "fix\F =
     (\<mu> x. fst (F\<cdot>(x, \<mu> y. snd (F\<cdot>(x, y)))),
      \<mu> y. snd (F\<cdot>(\<mu> x. fst (F\<cdot>(x, \<mu> y. snd (F\<cdot>(x, y)))), y)))"
  (is "fix\F = (?x, ?y)")
proof (rule fix_eqI)
  have *: "fst (F\(?x, ?y)) = ?x"
    by (rule trans [symmetric, OF fix_eq], simp)
  have "snd (F\(?x, ?y)) = ?y"
    by (rule trans [symmetric, OF fix_eq], simp)
  with * show "F\(?x, ?y) = (?x, ?y)"
    by (simp add: prod_eq_iff)
next
  fix z
  assume F_z: "F\z = z"
  obtain x y where z: "z = (x, y)" by (rule prod.exhaust)
  from F_z z have F_x: "fst (F\(x, y)) = x" by simp
  from F_z z have F_y: "snd (F\(x, y)) = y" by simp
  let ?y1 = "\ y. snd (F\(x, y))"
  have "?y1 \ y"
    by (rule fix_least) (simp add: F_y)
  then have "fst (F\(x, ?y1)) \ fst (F\(x, y))"
    by (simp add: fst_monofun monofun_cfun)
  with F_x have "fst (F\(x, ?y1)) \ x"
    by simp
  then have *: "?x \ x"
    by (simp add: fix_least_below)
  then have "snd (F\(?x, y)) \ snd (F\(x, y))"
    by (simp add: snd_monofun monofun_cfun)
  with F_y have "snd (F\(?x, y)) \ y"
    by simp
  then have "?y \ y"
    by (simp add: fix_least_below)
  with z * show "(?x, ?y) \ z"
    by simp
qed

section "Package for defining recursive functions in HOLCF"

subsection \<open>Pattern-match monad\<close>

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>

definition
  match_bottom :: "'a::pcpo \ 'c match \ 'c match"
where
  "match_bottom = (\ x k. seq\x\fail)"

definition
  match_Pair :: "'a \ 'b \ ('a \ 'b \ 'c match) \ 'c match"
where
  "match_Pair = (\ x k. csplit\k\x)"

definition
  match_spair :: "'a::pcpo \ 'b::pcpo \ ('a \ 'b \ 'c match) \ 'c::pcpo match"
where
  "match_spair = (\ x k. ssplit\k\x)"

definition
  match_sinl :: "'a::pcpo \ 'b::pcpo \ ('a \ 'c::pcpo match) \ 'c match"
where
  "match_sinl = (\ x k. sscase\k\(\ b. fail)\x)"

definition
  match_sinr :: "'a::pcpo \ 'b::pcpo \ ('b \ 'c::pcpo match) \ 'c match"
where
  "match_sinr = (\ x k. sscase\(\ a. fail)\k\x)"

definition
  match_up :: "'a u \ ('a \ 'c::pcpo match) \ 'c match"
where
  "match_up = (\ x k. fup\k\x)"

definition
  match_ONE :: "one \ 'c::pcpo match \ 'c match"
where
  "match_ONE = (\ ONE k. k)"

definition
  match_TT :: "tr \ 'c::pcpo match \ 'c match"
where
  "match_TT = (\ x k. If x then k else fail)"

definition
  match_FF :: "tr \ 'c::pcpo 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

quality100%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.