Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Concurrency_Monad.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/HOLCF/ex/Concurrency_Monad.thy
    Author:     Brian Huffman
*)

theory Concurrency_Monad
imports HOLCF
begin

text \<open>This file contains the concurrency monad example from
  Chapter 7 of the author's PhD thesis.\

subsection \<open>State/nondeterminism monad, as a type synonym\<close>

type_synonym ('s, 'a) N = "'s \ ('a u \ 's u)\"

definition mapN :: "('a \ 'b) \ ('s, 'a) N \ ('s, 'b) N"
  where "mapN = (\ f. cfun_map\ID\(convex_map\(sprod_map\(u_map\f)\ID)))"

definition unitN :: "'a \ ('s, 'a) N"
  where "unitN = (\ x. (\ s. convex_unit\(:up\x, up\s:)))"

definition bindN :: "('s, 'a) N \ ('a \ ('s, 'b) N) \ ('s, 'b) N"
  where "bindN = (\ c k. (\ s. convex_bind\(c\s)\(\ (:up\x, up\s':). k\x\s')))"

definition plusN :: "('s, 'a) N \ ('s, 'a) N \ ('s, 'a) N"
  where "plusN = (\ a b. (\ s. convex_plus\(a\s)\(b\s)))"

lemma mapN_ID: "mapN\ID = ID"
by (simp add: mapN_def domain_map_ID)

lemma mapN_mapN: "mapN\f\(mapN\g\m) = mapN\(\ x. f\(g\x))\m"
unfolding mapN_def ID_def
by (simp add: cfun_map_map convex_map_map sprod_map_map u_map_map eta_cfun)

lemma mapN_unitN: "mapN\f\(unitN\x) = unitN\(f\x)"
unfolding mapN_def unitN_def
by (simp add: cfun_map_def)

lemma bindN_unitN: "bindN\(unitN\a)\f = f\a"
by (simp add: unitN_def bindN_def eta_cfun)

lemma mapN_conv_bindN: "mapN\f\m = bindN\m\(unitN oo f)"
apply (simp add: mapN_def bindN_def unitN_def)
apply (rule cfun_eqI, simp)
apply (simp add: convex_map_def)
apply (rule cfun_arg_cong)
apply (rule cfun_eqI, simp, rename_tac p)
apply (case_tac p, simp)
apply (case_tac x, simp)
apply (case_tac y, simp)
apply simp
done

lemma bindN_unitN_right: "bindN\m\unitN = m"
proof -
  have "mapN\ID\m = m" by (simp add: mapN_ID)
  thus ?thesis by (simp add: mapN_conv_bindN)
qed

lemma bindN_bindN:
  "bindN\(bindN\m\f)\g = bindN\m\(\ x. bindN\(f\x)\g)"
apply (rule cfun_eqI, rename_tac s)
apply (simp add: bindN_def)
apply (simp add: convex_bind_bind)
apply (rule cfun_arg_cong)
apply (rule cfun_eqI, rename_tac w)
apply (case_tac w, simp)
apply (case_tac x, simp)
apply (case_tac y, simp)
apply simp
done

lemma mapN_bindN: "mapN\f\(bindN\m\g) = bindN\m\(\ x. mapN\f\(g\x))"
by (simp add: mapN_conv_bindN bindN_bindN)

lemma bindN_mapN: "bindN\(mapN\f\m)\g = bindN\m\(\ x. g\(f\x))"
by (simp add: mapN_conv_bindN bindN_bindN bindN_unitN)

lemma mapN_plusN:
  "mapN\f\(plusN\a\b) = plusN\(mapN\f\a)\(mapN\f\b)"
unfolding mapN_def plusN_def by (simp add: cfun_map_def)

lemma plusN_commute: "plusN\a\b = plusN\b\a"
unfolding plusN_def by (simp add: convex_plus_commute)

lemma plusN_assoc: "plusN\(plusN\a\b)\c = plusN\a\(plusN\b\c)"
unfolding plusN_def by (simp add: convex_plus_assoc)

lemma plusN_absorb: "plusN\a\a = a"
unfolding plusN_def by (simp add: eta_cfun)

subsection \<open>Resumption-state-nondeterminism monad\<close>

domain ('s, 'a) R = Done (lazy "'a") | More (lazy "('s, ('s, 'a) R) N")

thm R.take_induct

lemma R_induct [case_names adm bottom Done More, induct type: R]:
  fixes P :: "('s, 'a) R \ bool"
  assumes adm: "adm P"
  assumes bottom: "P \"
  assumes Done: "\x. P (Done\x)"
  assumes More: "\p c. (\r::('s, 'a) R. P (p\r)) \ P (More\(mapN\p\c))"
  shows "P r"
proof (induct r rule: R.take_induct)
  show "adm P" by fact
next
  fix n
  show "P (R_take n\r)"
  proof (induct n arbitrary: r)
    case 0 show ?case by (simp add: bottom)
  next
    case (Suc n r)
    show ?case
      apply (cases r)
      apply (simp add: bottom)
      apply (simp add: Done)
      using More [OF Suc]
      apply (simp add: mapN_def)
      done
  qed
qed

declare R.take_rews(2) [simp del]

lemma R_take_Suc_More [simp]:
  "R_take (Suc n)\(More\k) = More\(mapN\(R_take n)\k)"
by (simp add: mapN_def R.take_rews(2))

subsection \<open>Map function\<close>

fixrec mapR :: "('a \ 'b) \ ('s, 'a) R \ ('s, 'b) R"
  where "mapR\f\(Done\a) = Done\(f\a)"
  | "mapR\f\(More\k) = More\(mapN\(mapR\f)\k)"

lemma mapR_strict [simp]: "mapR\f\\ = \"
by fixrec_simp

lemma mapR_mapR: "mapR\f\(mapR\g\r) = mapR\(\ x. f\(g\x))\r"
by (induct r) (simp_all add: mapN_mapN)

lemma mapR_ID: "mapR\ID\r = r"
by (induct r) (simp_all add: mapN_mapN eta_cfun)

lemma "mapR\f\(mapR\g\r) = mapR\(\ x. f\(g\x))\r"
apply (induct r)
apply simp
apply simp
apply simp
apply (simp (no_asm))
apply (simp (no_asm) add: mapN_mapN)
apply simp
done

subsection \<open>Monadic bind function\<close>

fixrec bindR :: "('s, 'a) R \ ('a \ ('s, 'b) R) \ ('s, 'b) R"
  where "bindR\(Done\x)\k = k\x"
  | "bindR\(More\c)\k = More\(mapN\(\ r. bindR\r\k)\c)"

lemma bindR_strict [simp]: "bindR\\\k = \"
by fixrec_simp

lemma bindR_Done_right: "bindR\r\Done = r"
by (induct r) (simp_all add: mapN_mapN eta_cfun)

lemma mapR_conv_bindR: "mapR\f\r = bindR\r\(\ x. Done\(f\x))"
by (induct r) (simp_all add: mapN_mapN)

lemma bindR_bindR: "bindR\(bindR\r\f)\g = bindR\r\(\ x. bindR\(f\x)\g)"
by (induct r) (simp_all add: mapN_mapN)

lemma "bindR\(bindR\r\f)\g = bindR\r\(\ x. bindR\(f\x)\g)"
apply (induct r)
apply (simp_all add: mapN_mapN)
done

subsection \<open>Zip function\<close>

fixrec zipR :: "('a \ 'b \ 'c) \ ('s, 'a) R \ ('s, 'b) R \ ('s, 'c) R"
  where zipR_Done_Done:
    "zipR\f\(Done\x)\(Done\y) = Done\(f\x\y)"
  | zipR_Done_More:
    "zipR\f\(Done\x)\(More\b) =
      More\<cdot>(mapN\<cdot>(\<Lambda> r. zipR\<cdot>f\<cdot>(Done\<cdot>x)\<cdot>r)\<cdot>b)"
  | zipR_More_Done:
    "zipR\f\(More\a)\(Done\y) =
      More\<cdot>(mapN\<cdot>(\<Lambda> r. zipR\<cdot>f\<cdot>r\<cdot>(Done\<cdot>y))\<cdot>a)"
  | zipR_More_More:
    "zipR\f\(More\a)\(More\b) =
      More\<cdot>(plusN\<cdot>(mapN\<cdot>(\<Lambda> r. zipR\<cdot>f\<cdot>(More\<cdot>a)\<cdot>r)\<cdot>b)
                 \<cdot>(mapN\<cdot>(\<Lambda> r. zipR\<cdot>f\<cdot>r\<cdot>(More\<cdot>b))\<cdot>a))"

lemma zipR_strict1 [simp]: "zipR\f\\\r = \"
by fixrec_simp

lemma zipR_strict2 [simp]: "zipR\f\r\\ = \"
by (fixrec_simp, cases r, simp_all)

abbreviation apR (infixl "\" 70)
  where "a \ b \ zipR\ID\a\b"

text \<open>Proofs that \<open>zipR\<close> satisfies the applicative functor laws:\<close>

lemma R_homomorphism: "Done\f \ Done\x = Done\(f\x)"
  by simp

lemma R_identity: "Done\ID \ r = r"
  by (induct r, simp_all add: mapN_mapN eta_cfun)

lemma R_interchange: "r \ Done\x = Done\(\ f. f\x) \ r"
  by (induct r, simp_all add: mapN_mapN)

text \<open>The associativity rule is the hard one!\<close>

lemma R_associativity: "Done\cfcomp \ r1 \ r2 \ r3 = r1 \ (r2 \ r3)"
proof (induct r1 arbitrary: r2 r3)
  case (Done x1) thus ?case
  proof (induct r2 arbitrary: r3)
    case (Done x2) thus ?case
    proof (induct r3)
      case (More p3 c3) thus ?case (* Done/Done/More *)
        by (simp add: mapN_mapN)
    qed simp_all
  next
    case (More p2 c2) thus ?case
    proof (induct r3)
      case (Done x3) thus ?case (* Done/More/Done *)
        by (simp add: mapN_mapN)
    next
      case (More p3 c3) thus ?case (* Done/More/More *)
        by (simp add: mapN_mapN mapN_plusN)
    qed simp_all
  qed simp_all
next
  case (More p1 c1) thus ?case
  proof (induct r2 arbitrary: r3)
    case (Done y) thus ?case
    proof (induct r3)
      case (Done x3) thus ?case
        by (simp add: mapN_mapN)
    next
      case (More p3 c3) thus ?case
        by (simp add: mapN_mapN)
    qed simp_all
  next
    case (More p2 c2) thus ?case
    proof (induct r3)
      case (Done x3) thus ?case
        by (simp add: mapN_mapN mapN_plusN)
    next
      case (More p3 c3) thus ?case
        by (simp add: mapN_mapN mapN_plusN plusN_assoc)
    qed simp_all
  qed simp_all
qed simp_all

text \<open>Other miscellaneous properties about \<open>zipR\<close>:\<close>

lemma zipR_Done_left:
  shows "zipR\f\(Done\x)\r = mapR\(f\x)\r"
by (induct r) (simp_all add: mapN_mapN)

lemma zipR_Done_right:
  shows "zipR\f\r\(Done\y) = mapR\(\ x. f\x\y)\r"
by (induct r) (simp_all add: mapN_mapN)

lemma mapR_zipR: "mapR\h\(zipR\f\a\b) = zipR\(\ x y. h\(f\x\y))\a\b"
apply (induct a arbitrary: b)
apply simp
apply simp
apply (simp add: zipR_Done_left zipR_Done_right mapR_mapR)
apply (induct_tac b)
apply simp
apply simp
apply (simp add: mapN_mapN)
apply (simp add: mapN_mapN mapN_plusN)
done

lemma zipR_mapR_left: "zipR\f\(mapR\h\a)\b = zipR\(\ x y. f\(h\x)\y)\a\b"
apply (induct a arbitrary: b)
apply simp
apply simp
apply (simp add: zipR_Done_left zipR_Done_right eta_cfun)
apply (simp add: mapN_mapN)
apply (induct_tac b)
apply simp
apply simp
apply (simp add: mapN_mapN)
apply (simp add: mapN_mapN)
done

lemma zipR_mapR_right: "zipR\f\a\(mapR\h\b) = zipR\(\ x y. f\x\(h\y))\a\b"
apply (induct b arbitrary: a)
apply simp
apply simp
apply (simp add: zipR_Done_left zipR_Done_right)
apply (simp add: mapN_mapN)
apply (induct_tac a)
apply simp
apply simp
apply (simp add: mapN_mapN)
apply (simp add: mapN_mapN)
done

lemma zipR_commute:
  assumes f: "\x y. f\x\y = g\y\x"
  shows "zipR\f\a\b = zipR\g\b\a"
apply (induct a arbitrary: b)
apply simp
apply simp
apply (simp add: zipR_Done_left zipR_Done_right f [symmetric] eta_cfun)
apply (induct_tac b)
apply simp
apply simp
apply (simp add: mapN_mapN)
apply (simp add: mapN_mapN mapN_plusN plusN_commute)
done

lemma zipR_assoc:
  fixes a :: "('s, 'a) R" and b :: "('s, 'b) R" and c :: "('s, 'c) R"
  fixes f :: "'a \ 'b \ 'd" and g :: "'d \ 'c \ 'e"
  assumes gf: "\x y z. g\(f\x\y)\z = h\x\(k\y\z)"
  shows "zipR\g\(zipR\f\a\b)\c = zipR\h\a\(zipR\k\b\c)" (is "?P a b c")
apply (induct a arbitrary: b c)
    apply simp
   apply simp
  apply (simp add: zipR_Done_left zipR_Done_right)
  apply (simp add: zipR_mapR_left mapR_zipR gf)
apply (rename_tac pA kA b c)
apply (rule_tac x=c in spec)
apply (induct_tac b)
    apply simp
   apply simp
  apply (simp add: mapN_mapN)
  apply (simp add: zipR_Done_left zipR_Done_right eta_cfun)
  apply (simp add: zipR_mapR_right)
  apply (rule allI, rename_tac c)
  apply (induct_tac c)
     apply simp
    apply simp
   apply (rename_tac z)
   apply (simp add: mapN_mapN)
   apply (simp add: zipR_mapR_left gf)
  apply (rename_tac pC kC)
  apply (simp add: mapN_mapN)
  apply (simp add: zipR_mapR_left gf)
apply (rename_tac pB kB)
apply (rule allI, rename_tac c)
apply (induct_tac c)
    apply simp
   apply simp
  apply (simp add: mapN_mapN mapN_plusN)
apply (rename_tac pC kC)
apply (simp add: mapN_mapN mapN_plusN plusN_assoc)
done

text \<open>Alternative proof using take lemma.\<close>

lemma
  fixes a :: "('s, 'a) R" and b :: "('s, 'b) R" and c :: "('s, 'c) R"
  fixes f :: "'a \ 'b \ 'd" and g :: "'d \ 'c \ 'e"
  assumes gf: "\x y z. g\(f\x\y)\z = h\x\(k\y\z)"
  shows "zipR\g\(zipR\f\a\b)\c = zipR\h\a\(zipR\k\b\c)"
    (is "?lhs = ?rhs" is "?P a b c")
proof (rule R.take_lemma)
  fix n show "R_take n\?lhs = R_take n\?rhs"
  proof (induct n arbitrary: a b c)
    case (0 a b c)
    show ?case by simp
  next
    case (Suc n a b c)
    note IH = this
    let ?P = ?case
    show ?case
    proof (cases a)
      case bottom thus ?P by simp
    next
      case (Done x) thus ?P
        by (simp add: zipR_Done_left zipR_mapR_left mapR_zipR gf)
    next
      case (More nA) thus ?P
      proof (cases b)
        case bottom thus ?P by simp
      next
        case (Done y) thus ?P
          by (simp add: zipR_Done_left zipR_Done_right
            zipR_mapR_left zipR_mapR_right gf)
      next
        case (More nB) thus ?P
        proof (cases c)
          case bottom thus ?P by simp
        next
          case (Done z) thus ?P
            by (simp add: zipR_Done_right mapR_zipR zipR_mapR_right gf)
        next
          case (More nC)
          note H = \<open>a = More\<cdot>nA\<close> \<open>b = More\<cdot>nB\<close> \<open>c = More\<cdot>nC\<close>
          show ?P
            apply (simp only: H zipR_More_More)
            apply (simplesubst zipR_More_More [of f, symmetric])
            apply (simplesubst zipR_More_More [of k, symmetric])
            apply (simp only: H [symmetric])
            apply (simp add: mapN_mapN mapN_plusN plusN_assoc IH)
            done
        qed
      qed
    qed
  qed
qed

end

¤ Dauer der Verarbeitung: 0.3 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.