src/HOL/HOLCF/ex/Concurrency_Monad.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 43524 d75e285fcf3e
child 62110 8d75ff14e3e9
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43524
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
     1
(*  Title:      HOL/HOLCF/ex/Concurrency_Monad.thy
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
     3
*)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
     4
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
     5
theory Concurrency_Monad
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
     6
imports HOLCF
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
     7
begin
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
     8
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
     9
text {* This file contains the concurrency monad example from
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    10
  Chapter 7 of the author's PhD thesis. *}
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    11
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    12
subsection {* State/nondeterminism monad, as a type synonym *}
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    13
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    14
type_synonym ('s, 'a) N = "'s \<rightarrow> ('a u \<otimes> 's u)\<natural>"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    15
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    16
definition mapN :: "('a \<rightarrow> 'b) \<rightarrow> ('s, 'a) N \<rightarrow> ('s, 'b) N"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    17
  where "mapN = (\<Lambda> f. cfun_map\<cdot>ID\<cdot>(convex_map\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>ID)))"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    18
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    19
definition unitN :: "'a \<rightarrow> ('s, 'a) N"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    20
  where "unitN = (\<Lambda> x. (\<Lambda> s. convex_unit\<cdot>(:up\<cdot>x, up\<cdot>s:)))"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    21
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    22
definition bindN :: "('s, 'a) N \<rightarrow> ('a \<rightarrow> ('s, 'b) N) \<rightarrow> ('s, 'b) N"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    23
  where "bindN = (\<Lambda> c k. (\<Lambda> s. convex_bind\<cdot>(c\<cdot>s)\<cdot>(\<Lambda> (:up\<cdot>x, up\<cdot>s':). k\<cdot>x\<cdot>s')))"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    24
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    25
definition plusN :: "('s, 'a) N \<rightarrow> ('s, 'a) N \<rightarrow> ('s, 'a) N"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    26
  where "plusN = (\<Lambda> a b. (\<Lambda> s. convex_plus\<cdot>(a\<cdot>s)\<cdot>(b\<cdot>s)))"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    27
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    28
lemma mapN_ID: "mapN\<cdot>ID = ID"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    29
by (simp add: mapN_def domain_map_ID)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    30
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    31
lemma mapN_mapN: "mapN\<cdot>f\<cdot>(mapN\<cdot>g\<cdot>m) = mapN\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>m"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    32
unfolding mapN_def ID_def
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    33
by (simp add: cfun_map_map convex_map_map sprod_map_map u_map_map eta_cfun)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    34
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    35
lemma mapN_unitN: "mapN\<cdot>f\<cdot>(unitN\<cdot>x) = unitN\<cdot>(f\<cdot>x)"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    36
unfolding mapN_def unitN_def
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    37
by (simp add: cfun_map_def)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    38
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    39
lemma bindN_unitN: "bindN\<cdot>(unitN\<cdot>a)\<cdot>f = f\<cdot>a"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    40
by (simp add: unitN_def bindN_def eta_cfun)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    41
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    42
lemma mapN_conv_bindN: "mapN\<cdot>f\<cdot>m = bindN\<cdot>m\<cdot>(unitN oo f)"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    43
apply (simp add: mapN_def bindN_def unitN_def)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    44
apply (rule cfun_eqI, simp)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    45
apply (simp add: convex_map_def)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    46
apply (rule cfun_arg_cong)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    47
apply (rule cfun_eqI, simp, rename_tac p)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    48
apply (case_tac p, simp)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    49
apply (case_tac x, simp)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    50
apply (case_tac y, simp)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    51
apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    52
done
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    53
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    54
lemma bindN_unitN_right: "bindN\<cdot>m\<cdot>unitN = m"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    55
proof -
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    56
  have "mapN\<cdot>ID\<cdot>m = m" by (simp add: mapN_ID)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    57
  thus ?thesis by (simp add: mapN_conv_bindN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    58
qed
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    59
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    60
lemma bindN_bindN:
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    61
  "bindN\<cdot>(bindN\<cdot>m\<cdot>f)\<cdot>g = bindN\<cdot>m\<cdot>(\<Lambda> x. bindN\<cdot>(f\<cdot>x)\<cdot>g)"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    62
apply (rule cfun_eqI, rename_tac s)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    63
apply (simp add: bindN_def)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    64
apply (simp add: convex_bind_bind)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    65
apply (rule cfun_arg_cong)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    66
apply (rule cfun_eqI, rename_tac w)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    67
apply (case_tac w, simp)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    68
apply (case_tac x, simp)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    69
apply (case_tac y, simp)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    70
apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    71
done
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    72
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    73
lemma mapN_bindN: "mapN\<cdot>f\<cdot>(bindN\<cdot>m\<cdot>g) = bindN\<cdot>m\<cdot>(\<Lambda> x. mapN\<cdot>f\<cdot>(g\<cdot>x))"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    74
by (simp add: mapN_conv_bindN bindN_bindN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    75
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    76
lemma bindN_mapN: "bindN\<cdot>(mapN\<cdot>f\<cdot>m)\<cdot>g = bindN\<cdot>m\<cdot>(\<Lambda> x. g\<cdot>(f\<cdot>x))"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    77
by (simp add: mapN_conv_bindN bindN_bindN bindN_unitN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    78
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    79
lemma mapN_plusN:
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    80
  "mapN\<cdot>f\<cdot>(plusN\<cdot>a\<cdot>b) = plusN\<cdot>(mapN\<cdot>f\<cdot>a)\<cdot>(mapN\<cdot>f\<cdot>b)"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    81
unfolding mapN_def plusN_def by (simp add: cfun_map_def)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    82
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    83
lemma plusN_commute: "plusN\<cdot>a\<cdot>b = plusN\<cdot>b\<cdot>a"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    84
unfolding plusN_def by (simp add: convex_plus_commute)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    85
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    86
lemma plusN_assoc: "plusN\<cdot>(plusN\<cdot>a\<cdot>b)\<cdot>c = plusN\<cdot>a\<cdot>(plusN\<cdot>b\<cdot>c)"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    87
unfolding plusN_def by (simp add: convex_plus_assoc)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    88
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    89
lemma plusN_absorb: "plusN\<cdot>a\<cdot>a = a"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    90
unfolding plusN_def by (simp add: eta_cfun)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    91
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    92
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    93
subsection {* Resumption-state-nondeterminism monad *}
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    94
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    95
domain ('s, 'a) R = Done (lazy "'a") | More (lazy "('s, ('s, 'a) R) N")
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    96
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    97
thm R.take_induct
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    98
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
    99
lemma R_induct [case_names adm bottom Done More, induct type: R]:
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   100
  fixes P :: "('s, 'a) R \<Rightarrow> bool"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   101
  assumes adm: "adm P"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   102
  assumes bottom: "P \<bottom>"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   103
  assumes Done: "\<And>x. P (Done\<cdot>x)"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   104
  assumes More: "\<And>p c. (\<And>r::('s, 'a) R. P (p\<cdot>r)) \<Longrightarrow> P (More\<cdot>(mapN\<cdot>p\<cdot>c))"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   105
  shows "P r"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   106
proof (induct r rule: R.take_induct)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   107
  show "adm P" by fact
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   108
next
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   109
  fix n
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   110
  show "P (R_take n\<cdot>r)"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   111
  proof (induct n arbitrary: r)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   112
    case 0 show ?case by (simp add: bottom)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   113
  next
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   114
    case (Suc n r)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   115
    show ?case
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   116
      apply (cases r)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   117
      apply (simp add: bottom)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   118
      apply (simp add: Done)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   119
      using More [OF Suc]
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   120
      apply (simp add: mapN_def)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   121
      done
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   122
  qed
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   123
qed
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   124
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   125
declare R.take_rews(2) [simp del]
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   126
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   127
lemma R_take_Suc_More [simp]:
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   128
  "R_take (Suc n)\<cdot>(More\<cdot>k) = More\<cdot>(mapN\<cdot>(R_take n)\<cdot>k)"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   129
by (simp add: mapN_def R.take_rews(2))
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   130
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   131
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   132
subsection {* Map function *}
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   133
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   134
fixrec mapR :: "('a \<rightarrow> 'b) \<rightarrow> ('s, 'a) R \<rightarrow> ('s, 'b) R"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   135
  where "mapR\<cdot>f\<cdot>(Done\<cdot>a) = Done\<cdot>(f\<cdot>a)"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   136
  | "mapR\<cdot>f\<cdot>(More\<cdot>k) = More\<cdot>(mapN\<cdot>(mapR\<cdot>f)\<cdot>k)"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   137
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   138
lemma mapR_strict [simp]: "mapR\<cdot>f\<cdot>\<bottom> = \<bottom>"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   139
by fixrec_simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   140
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   141
lemma mapR_mapR: "mapR\<cdot>f\<cdot>(mapR\<cdot>g\<cdot>r) = mapR\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>r"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   142
by (induct r) (simp_all add: mapN_mapN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   143
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   144
lemma mapR_ID: "mapR\<cdot>ID\<cdot>r = r"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   145
by (induct r) (simp_all add: mapN_mapN eta_cfun)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   146
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   147
lemma "mapR\<cdot>f\<cdot>(mapR\<cdot>g\<cdot>r) = mapR\<cdot>(\<Lambda> x. f\<cdot>(g\<cdot>x))\<cdot>r"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   148
apply (induct r)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   149
apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   150
apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   151
apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   152
apply (simp (no_asm))
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   153
apply (simp (no_asm) add: mapN_mapN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   154
apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   155
done
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   156
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   157
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   158
subsection {* Monadic bind function *}
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   159
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   160
fixrec bindR :: "('s, 'a) R \<rightarrow> ('a \<rightarrow> ('s, 'b) R) \<rightarrow> ('s, 'b) R"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   161
  where "bindR\<cdot>(Done\<cdot>x)\<cdot>k = k\<cdot>x"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   162
  | "bindR\<cdot>(More\<cdot>c)\<cdot>k = More\<cdot>(mapN\<cdot>(\<Lambda> r. bindR\<cdot>r\<cdot>k)\<cdot>c)"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   163
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   164
lemma bindR_strict [simp]: "bindR\<cdot>\<bottom>\<cdot>k = \<bottom>"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   165
by fixrec_simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   166
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   167
lemma bindR_Done_right: "bindR\<cdot>r\<cdot>Done = r"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   168
by (induct r) (simp_all add: mapN_mapN eta_cfun)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   169
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   170
lemma mapR_conv_bindR: "mapR\<cdot>f\<cdot>r = bindR\<cdot>r\<cdot>(\<Lambda> x. Done\<cdot>(f\<cdot>x))"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   171
by (induct r) (simp_all add: mapN_mapN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   172
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   173
lemma bindR_bindR: "bindR\<cdot>(bindR\<cdot>r\<cdot>f)\<cdot>g = bindR\<cdot>r\<cdot>(\<Lambda> x. bindR\<cdot>(f\<cdot>x)\<cdot>g)"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   174
by (induct r) (simp_all add: mapN_mapN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   175
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   176
lemma "bindR\<cdot>(bindR\<cdot>r\<cdot>f)\<cdot>g = bindR\<cdot>r\<cdot>(\<Lambda> x. bindR\<cdot>(f\<cdot>x)\<cdot>g)"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   177
apply (induct r)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   178
apply (simp_all add: mapN_mapN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   179
done
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   180
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   181
subsection {* Zip function *}
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   182
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   183
fixrec zipR :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('s, 'a) R \<rightarrow> ('s, 'b) R \<rightarrow> ('s, 'c) R"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   184
  where zipR_Done_Done:
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   185
    "zipR\<cdot>f\<cdot>(Done\<cdot>x)\<cdot>(Done\<cdot>y) = Done\<cdot>(f\<cdot>x\<cdot>y)"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   186
  | zipR_Done_More:
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   187
    "zipR\<cdot>f\<cdot>(Done\<cdot>x)\<cdot>(More\<cdot>b) =
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   188
      More\<cdot>(mapN\<cdot>(\<Lambda> r. zipR\<cdot>f\<cdot>(Done\<cdot>x)\<cdot>r)\<cdot>b)"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   189
  | zipR_More_Done:
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   190
    "zipR\<cdot>f\<cdot>(More\<cdot>a)\<cdot>(Done\<cdot>y) =
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   191
      More\<cdot>(mapN\<cdot>(\<Lambda> r. zipR\<cdot>f\<cdot>r\<cdot>(Done\<cdot>y))\<cdot>a)"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   192
  | zipR_More_More:
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   193
    "zipR\<cdot>f\<cdot>(More\<cdot>a)\<cdot>(More\<cdot>b) =
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   194
      More\<cdot>(plusN\<cdot>(mapN\<cdot>(\<Lambda> r. zipR\<cdot>f\<cdot>(More\<cdot>a)\<cdot>r)\<cdot>b)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   195
                 \<cdot>(mapN\<cdot>(\<Lambda> r. zipR\<cdot>f\<cdot>r\<cdot>(More\<cdot>b))\<cdot>a))"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   196
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   197
lemma zipR_strict1 [simp]: "zipR\<cdot>f\<cdot>\<bottom>\<cdot>r = \<bottom>"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   198
by fixrec_simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   199
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   200
lemma zipR_strict2 [simp]: "zipR\<cdot>f\<cdot>r\<cdot>\<bottom> = \<bottom>"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   201
by (fixrec_simp, cases r, simp_all)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   202
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   203
abbreviation apR (infixl "\<diamond>" 70)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   204
  where "a \<diamond> b \<equiv> zipR\<cdot>ID\<cdot>a\<cdot>b"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   205
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   206
text {* Proofs that @{text zipR} satisfies the applicative functor laws: *}
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   207
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   208
lemma R_homomorphism: "Done\<cdot>f \<diamond> Done\<cdot>x = Done\<cdot>(f\<cdot>x)"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   209
  by simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   210
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   211
lemma R_identity: "Done\<cdot>ID \<diamond> r = r"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   212
  by (induct r, simp_all add: mapN_mapN eta_cfun)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   213
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   214
lemma R_interchange: "r \<diamond> Done\<cdot>x = Done\<cdot>(\<Lambda> f. f\<cdot>x) \<diamond> r"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   215
  by (induct r, simp_all add: mapN_mapN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   216
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   217
text {* The associativity rule is the hard one! *}
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   218
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   219
lemma R_associativity: "Done\<cdot>cfcomp \<diamond> r1 \<diamond> r2 \<diamond> r3 = r1 \<diamond> (r2 \<diamond> r3)"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   220
proof (induct r1 arbitrary: r2 r3)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   221
  case (Done x1) thus ?case
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   222
  proof (induct r2 arbitrary: r3)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   223
    case (Done x2) thus ?case
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   224
    proof (induct r3)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   225
      case (More p3 c3) thus ?case (* Done/Done/More *)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   226
        by (simp add: mapN_mapN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   227
    qed simp_all
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   228
  next
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   229
    case (More p2 c2) thus ?case
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   230
    proof (induct r3)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   231
      case (Done x3) thus ?case (* Done/More/Done *)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   232
        by (simp add: mapN_mapN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   233
    next
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   234
      case (More p3 c3) thus ?case (* Done/More/More *)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   235
        by (simp add: mapN_mapN mapN_plusN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   236
    qed simp_all
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   237
  qed simp_all
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   238
next
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   239
  case (More p1 c1) thus ?case
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   240
  proof (induct r2 arbitrary: r3)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   241
    case (Done y) thus ?case
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   242
    proof (induct r3)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   243
      case (Done x3) thus ?case
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   244
        by (simp add: mapN_mapN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   245
    next
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   246
      case (More p3 c3) thus ?case
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   247
        by (simp add: mapN_mapN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   248
    qed simp_all
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   249
  next
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   250
    case (More p2 c2) thus ?case
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   251
    proof (induct r3)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   252
      case (Done x3) thus ?case
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   253
        by (simp add: mapN_mapN mapN_plusN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   254
    next
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   255
      case (More p3 c3) thus ?case
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   256
        by (simp add: mapN_mapN mapN_plusN plusN_assoc)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   257
    qed simp_all
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   258
  qed simp_all
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   259
qed simp_all
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   260
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   261
text {* Other miscellaneous properties about @{text zipR}: *}
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   262
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   263
lemma zipR_Done_left:
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   264
  shows "zipR\<cdot>f\<cdot>(Done\<cdot>x)\<cdot>r = mapR\<cdot>(f\<cdot>x)\<cdot>r"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   265
by (induct r) (simp_all add: mapN_mapN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   266
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   267
lemma zipR_Done_right:
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   268
  shows "zipR\<cdot>f\<cdot>r\<cdot>(Done\<cdot>y) = mapR\<cdot>(\<Lambda> x. f\<cdot>x\<cdot>y)\<cdot>r"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   269
by (induct r) (simp_all add: mapN_mapN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   270
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   271
lemma mapR_zipR: "mapR\<cdot>h\<cdot>(zipR\<cdot>f\<cdot>a\<cdot>b) = zipR\<cdot>(\<Lambda> x y. h\<cdot>(f\<cdot>x\<cdot>y))\<cdot>a\<cdot>b"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   272
apply (induct a arbitrary: b)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   273
apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   274
apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   275
apply (simp add: zipR_Done_left zipR_Done_right mapR_mapR)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   276
apply (induct_tac b)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   277
apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   278
apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   279
apply (simp add: mapN_mapN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   280
apply (simp add: mapN_mapN mapN_plusN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   281
done
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   282
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   283
lemma zipR_mapR_left: "zipR\<cdot>f\<cdot>(mapR\<cdot>h\<cdot>a)\<cdot>b = zipR\<cdot>(\<Lambda> x y. f\<cdot>(h\<cdot>x)\<cdot>y)\<cdot>a\<cdot>b"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   284
apply (induct a arbitrary: b)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   285
apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   286
apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   287
apply (simp add: zipR_Done_left zipR_Done_right eta_cfun)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   288
apply (simp add: mapN_mapN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   289
apply (induct_tac b)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   290
apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   291
apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   292
apply (simp add: mapN_mapN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   293
apply (simp add: mapN_mapN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   294
done
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   295
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   296
lemma zipR_mapR_right: "zipR\<cdot>f\<cdot>a\<cdot>(mapR\<cdot>h\<cdot>b) = zipR\<cdot>(\<Lambda> x y. f\<cdot>x\<cdot>(h\<cdot>y))\<cdot>a\<cdot>b"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   297
apply (induct b arbitrary: a)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   298
apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   299
apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   300
apply (simp add: zipR_Done_left zipR_Done_right)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   301
apply (simp add: mapN_mapN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   302
apply (induct_tac a)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   303
apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   304
apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   305
apply (simp add: mapN_mapN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   306
apply (simp add: mapN_mapN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   307
done
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   308
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   309
lemma zipR_commute:
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   310
  assumes f: "\<And>x y. f\<cdot>x\<cdot>y = g\<cdot>y\<cdot>x"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   311
  shows "zipR\<cdot>f\<cdot>a\<cdot>b = zipR\<cdot>g\<cdot>b\<cdot>a"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   312
apply (induct a arbitrary: b)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   313
apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   314
apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   315
apply (simp add: zipR_Done_left zipR_Done_right f [symmetric] eta_cfun)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   316
apply (induct_tac b)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   317
apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   318
apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   319
apply (simp add: mapN_mapN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   320
apply (simp add: mapN_mapN mapN_plusN plusN_commute)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   321
done
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   322
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   323
lemma zipR_assoc:
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   324
  fixes a :: "('s, 'a) R" and b :: "('s, 'b) R" and c :: "('s, 'c) R"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   325
  fixes f :: "'a \<rightarrow> 'b \<rightarrow> 'd" and g :: "'d \<rightarrow> 'c \<rightarrow> 'e"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   326
  assumes gf: "\<And>x y z. g\<cdot>(f\<cdot>x\<cdot>y)\<cdot>z = h\<cdot>x\<cdot>(k\<cdot>y\<cdot>z)"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   327
  shows "zipR\<cdot>g\<cdot>(zipR\<cdot>f\<cdot>a\<cdot>b)\<cdot>c = zipR\<cdot>h\<cdot>a\<cdot>(zipR\<cdot>k\<cdot>b\<cdot>c)" (is "?P a b c")
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   328
 apply (induct a arbitrary: b c)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   329
    apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   330
   apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   331
  apply (simp add: zipR_Done_left zipR_Done_right)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   332
  apply (simp add: zipR_mapR_left mapR_zipR gf)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   333
 apply (rename_tac pA kA b c)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   334
 apply (rule_tac x=c in spec)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   335
 apply (induct_tac b)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   336
    apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   337
   apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   338
  apply (simp add: mapN_mapN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   339
  apply (simp add: zipR_Done_left zipR_Done_right eta_cfun)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   340
  apply (simp add: zipR_mapR_right)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   341
  apply (rule allI, rename_tac c)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   342
  apply (induct_tac c)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   343
     apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   344
    apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   345
   apply (rename_tac z)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   346
   apply (simp add: mapN_mapN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   347
   apply (simp add: zipR_mapR_left gf)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   348
  apply (rename_tac pC kC)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   349
  apply (simp add: mapN_mapN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   350
  apply (simp add: zipR_mapR_left gf)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   351
 apply (rename_tac pB kB)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   352
 apply (rule allI, rename_tac c)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   353
 apply (induct_tac c)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   354
    apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   355
   apply simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   356
  apply (simp add: mapN_mapN mapN_plusN)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   357
 apply (rename_tac pC kC)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   358
 apply (simp add: mapN_mapN mapN_plusN plusN_assoc)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   359
done
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   360
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   361
text {* Alternative proof using take lemma. *}
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   362
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   363
lemma
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   364
  fixes a :: "('s, 'a) R" and b :: "('s, 'b) R" and c :: "('s, 'c) R"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   365
  fixes f :: "'a \<rightarrow> 'b \<rightarrow> 'd" and g :: "'d \<rightarrow> 'c \<rightarrow> 'e"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   366
  assumes gf: "\<And>x y z. g\<cdot>(f\<cdot>x\<cdot>y)\<cdot>z = h\<cdot>x\<cdot>(k\<cdot>y\<cdot>z)"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   367
  shows "zipR\<cdot>g\<cdot>(zipR\<cdot>f\<cdot>a\<cdot>b)\<cdot>c = zipR\<cdot>h\<cdot>a\<cdot>(zipR\<cdot>k\<cdot>b\<cdot>c)"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   368
    (is "?lhs = ?rhs" is "?P a b c")
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   369
proof (rule R.take_lemma)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   370
  fix n show "R_take n\<cdot>?lhs = R_take n\<cdot>?rhs"
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   371
  proof (induct n arbitrary: a b c)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   372
    case (0 a b c)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   373
    show ?case by simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   374
  next
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   375
    case (Suc n a b c)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   376
    note IH = this
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   377
    let ?P = ?case
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   378
    show ?case
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   379
    proof (cases a)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   380
      case bottom thus ?P by simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   381
    next
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   382
      case (Done x) thus ?P
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   383
        by (simp add: zipR_Done_left zipR_mapR_left mapR_zipR gf)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   384
    next
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   385
      case (More nA) thus ?P
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   386
      proof (cases b)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   387
        case bottom thus ?P by simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   388
      next
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   389
        case (Done y) thus ?P
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   390
          by (simp add: zipR_Done_left zipR_Done_right
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   391
            zipR_mapR_left zipR_mapR_right gf)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   392
      next
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   393
        case (More nB) thus ?P
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   394
        proof (cases c)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   395
          case bottom thus ?P by simp
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   396
        next
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   397
          case (Done z) thus ?P
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   398
            by (simp add: zipR_Done_right mapR_zipR zipR_mapR_right gf)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   399
        next
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   400
          case (More nC)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   401
          note H = `a = More\<cdot>nA` `b = More\<cdot>nB` `c = More\<cdot>nC`
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   402
          show ?P
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   403
            apply (simp only: H zipR_More_More)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   404
            apply (simplesubst zipR_More_More [of f, symmetric])
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   405
            apply (simplesubst zipR_More_More [of k, symmetric])
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   406
            apply (simp only: H [symmetric])
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   407
            apply (simp add: mapN_mapN mapN_plusN plusN_assoc IH)
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   408
            done
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   409
        qed
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   410
      qed
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   411
    qed
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   412
  qed
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   413
qed
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   414
d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
diff changeset
   415
end