author  haftmann 
Fri, 17 Jun 2005 16:12:49 +0200  
changeset 16417  9bc16273c2d4 
parent 16401  57c35ede00b9 
child 16460  72a08d509d62 
permissions  rwrr 
16221  1 
(* Title: HOLCF/Fixrec.thy 
2 
ID: $Id$ 

3 
Author: Amber Telfer and Brian Huffman 

4 
*) 

5 

6 
header "Package for defining recursive functions in HOLCF" 

7 

8 
theory Fixrec 

9 
imports Ssum One Up Fix 

16417  10 
uses ("fixrec_package.ML") 
16221  11 
begin 
12 

13 
subsection {* Maybe monad type *} 

14 

15 
types 'a maybe = "one ++ 'a u" 

16 

17 
constdefs 

18 
fail :: "'a maybe" 

19 
"fail \<equiv> sinl\<cdot>ONE" 

20 

21 
return :: "'a \<rightarrow> 'a maybe" 

22 
"return \<equiv> sinr oo up" 

23 

24 
lemma maybeE: 

25 
"\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = fail \<Longrightarrow> Q; \<And>x. p = return\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" 

26 
apply (unfold fail_def return_def) 

27 
apply (rule_tac p=p in ssumE, simp) 

28 
apply (rule_tac p=x in oneE, simp, simp) 

29 
apply (rule_tac p=y in upE1, simp, simp) 

30 
done 

31 

32 
subsection {* Monadic bind operator *} 

33 

34 
constdefs 

35 
bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe" 

36 
"bind \<equiv> \<Lambda> m f. sscase\<cdot>sinl\<cdot>(fup\<cdot>f)\<cdot>m" 

37 

38 
syntax 

39 
"_bind" :: "'a maybe \<Rightarrow> ('a \<rightarrow> 'b maybe) \<Rightarrow> 'b maybe" 

40 
("(_ >>= _)" [50, 51] 50) 

41 

42 
translations "m >>= k" == "bind\<cdot>m\<cdot>k" 

43 

44 
nonterminals 

45 
maybebind maybebinds 

46 

47 
syntax 

48 
"_MBIND" :: "pttrn \<Rightarrow> 'a maybe \<Rightarrow> maybebind" ("(2_ </ _)" 10) 

49 
"" :: "maybebind \<Rightarrow> maybebinds" ("_") 

50 

51 
"_MBINDS" :: "[maybebind, maybebinds] \<Rightarrow> maybebinds" ("_;/ _") 

52 
"_MDO" :: "[maybebinds, 'a maybe] \<Rightarrow> 'a maybe" ("(do _;/ (_))" 10) 

53 

54 
translations 

55 
"_MDO (_MBINDS b bs) e" == "_MDO b (_MDO bs e)" 

56 
"do (x,y) < m; e" == "m >>= (LAM <x,y>. e)" 

57 
"do x < m; e" == "m >>= (LAM x. e)" 

58 

59 
text {* monad laws *} 

60 

61 
lemma bind_strict [simp]: "UU >>= f = UU" 

62 
by (simp add: bind_def) 

63 

64 
lemma bind_fail [simp]: "fail >>= f = fail" 

65 
by (simp add: bind_def fail_def) 

66 

67 
lemma left_unit [simp]: "(return\<cdot>a) >>= k = k\<cdot>a" 

68 
by (simp add: bind_def return_def) 

69 

70 
lemma right_unit [simp]: "m >>= return = m" 

71 
by (rule_tac p=m in maybeE, simp_all) 

72 

73 
lemma bind_assoc [simp]: 

74 
"(do a < m; b < k\<cdot>a; h\<cdot>b) = (do b < (do a < m; k\<cdot>a); h\<cdot>b)" 

75 
by (rule_tac p=m in maybeE, simp_all) 

76 

77 
subsection {* Run operator *} 

78 

79 
constdefs 

80 
run:: "'a maybe \<rightarrow> 'a" 

81 
"run \<equiv> sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)" 

82 

83 
text {* rewrite rules for run *} 

84 

85 
lemma run_strict [simp]: "run\<cdot>\<bottom> = \<bottom>" 

86 
by (simp add: run_def) 

87 

88 
lemma run_fail [simp]: "run\<cdot>fail = \<bottom>" 

89 
by (simp add: run_def fail_def) 

90 

91 
lemma run_return [simp]: "run\<cdot>(return\<cdot>x) = x" 

92 
by (simp add: run_def return_def) 

93 

94 
subsection {* Monad plus operator *} 

95 

96 
constdefs 

97 
mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe" 

98 
"mplus \<equiv> \<Lambda> m1 m2. sscase\<cdot>(\<Lambda> x. m2)\<cdot>(fup\<cdot>return)\<cdot>m1" 

99 

100 
syntax "+++" :: "'a maybe \<Rightarrow> 'a maybe \<Rightarrow> 'a maybe" (infixr 65) 

101 
translations "x +++ y" == "mplus\<cdot>x\<cdot>y" 

102 

103 
text {* rewrite rules for mplus *} 

104 

105 
lemma mplus_strict [simp]: "\<bottom> +++ m = \<bottom>" 

106 
by (simp add: mplus_def) 

107 

108 
lemma mplus_fail [simp]: "fail +++ m = m" 

109 
by (simp add: mplus_def fail_def) 

110 

111 
lemma mplus_return [simp]: "return\<cdot>x +++ m = return\<cdot>x" 

112 
by (simp add: mplus_def return_def) 

113 

114 
lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)" 

115 
by (rule_tac p=x in maybeE, simp_all) 

116 

117 
subsection {* Match functions for builtin types *} 

118 

119 
text {* Currently the package only supports lazy constructors *} 

120 

121 
constdefs 

122 
match_cpair :: "'a \<times> 'b \<rightarrow> ('a \<times> 'b) maybe" 

123 
"match_cpair \<equiv> csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)" 

124 

125 
match_up :: "'a u \<rightarrow> 'a maybe" 

126 
"match_up \<equiv> fup\<cdot>return" 

127 

128 
lemma match_cpair_simps [simp]: 

129 
"match_cpair\<cdot><x,y> = return\<cdot><x,y>" 

130 
by (simp add: match_cpair_def) 

131 

132 
lemma match_up_simps [simp]: 

133 
"match_up\<cdot>(up\<cdot>x) = return\<cdot>x" 

134 
"match_up\<cdot>\<bottom> = \<bottom>" 

135 
by (simp_all add: match_up_def) 

136 

16401
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

137 
subsection {* Mutual recursion *} 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

138 

57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

139 
text {* 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

140 
The following rules are used to prove unfolding theorems from 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

141 
fixedpoint definitions of mutually recursive functions. 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

142 
*} 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

143 

57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

144 
lemma cpair_equalI: "\<lbrakk>x \<equiv> cfst\<cdot>p; y \<equiv> csnd\<cdot>p\<rbrakk> \<Longrightarrow> <x,y> \<equiv> p" 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

145 
by (simp add: surjective_pairing_Cprod2) 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

146 

57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

147 
lemma cpair_eqD1: "<x,y> = <x',y'> \<Longrightarrow> x = x'" 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

148 
by simp 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

149 

57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

150 
lemma cpair_eqD2: "<x,y> = <x',y'> \<Longrightarrow> y = y'" 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

151 
by simp 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

152 

57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

153 
ML {* 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

154 
val cpair_equalI = thm "cpair_equalI"; 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

155 
val cpair_eqD1 = thm "cpair_eqD1"; 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

156 
val cpair_eqD2 = thm "cpair_eqD2"; 
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

157 
*} 
16221  158 

159 
subsection {* Intitializing the fixrec package *} 

160 

16229  161 
use "fixrec_package.ML" 
16221  162 

163 
end 