Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Fix.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/HOLCF/Fix.thy
    Author:     Franz Regensburger
    Author:     Brian Huffman
*)

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

theory Fix
  imports Cfun
begin

default_sort pcpo

subsection \<open>Iteration\<close>

primrec iterate :: "nat \ ('a::cpo \ '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 \ 'a) \ 'a"
  where "fix = (\ F. \i. iterate i\F\\)"

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

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

notation (ASCII)
  fix_syn  (binder "FIX " 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:
  "fix\(F::'a \ 'b \ 'a \ 'b) =
   (\<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

end

¤ Dauer der Verarbeitung: 0.4 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.