author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 43524  d75e285fcf3e 
child 62110  8d75ff14e3e9 
permissions  rwrr 
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 {* Resumptionstatenondeterminism 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 