author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 23152  9497234a2743 
child 25131  2c8caac48ade 
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 

16551  9 
imports Sprod Ssum Up One Tr Fix 
23152  10 
uses ("Tools/fixrec_package.ML") 
16221  11 
begin 
12 

13 
subsection {* Maybe monad type *} 

14 

16776
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

15 
defaultsort cpo 
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

16 

19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

17 
pcpodef (open) 'a maybe = "UNIV::(one ++ 'a u) set" 
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

18 
by simp 
16221  19 

20 
constdefs 

21 
fail :: "'a maybe" 

19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

22 
"fail \<equiv> Abs_maybe (sinl\<cdot>ONE)" 
16221  23 

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

19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

25 
"return \<equiv> \<Lambda> x. Abs_maybe (sinr\<cdot>(up\<cdot>x))" 
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

26 

e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

27 
maybe_when :: "'b \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a maybe \<rightarrow> 'b::pcpo" 
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

28 
"maybe_when \<equiv> \<Lambda> f r m. sscase\<cdot>(\<Lambda> x. f)\<cdot>(fup\<cdot>r)\<cdot>(Rep_maybe m)" 
16221  29 

30 
lemma maybeE: 

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

32 
apply (unfold fail_def return_def) 

19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

33 
apply (cases p, rename_tac r) 
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

34 
apply (rule_tac p=r in ssumE, simp add: Abs_maybe_strict) 
16221  35 
apply (rule_tac p=x in oneE, simp, simp) 
19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

36 
apply (rule_tac p=y in upE, simp, simp add: cont_Abs_maybe) 
16221  37 
done 
38 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

39 
lemma return_defined [simp]: "return\<cdot>x \<noteq> \<bottom>" 
19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

40 
by (simp add: return_def cont_Abs_maybe Abs_maybe_defined) 
18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

41 

4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

42 
lemma fail_defined [simp]: "fail \<noteq> \<bottom>" 
19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

43 
by (simp add: fail_def Abs_maybe_defined) 
18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

44 

4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

45 
lemma return_eq [simp]: "(return\<cdot>x = return\<cdot>y) = (x = y)" 
19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

46 
by (simp add: return_def cont_Abs_maybe Abs_maybe_inject) 
18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

47 

4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

48 
lemma return_neq_fail [simp]: 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

49 
"return\<cdot>x \<noteq> fail" "fail \<noteq> return\<cdot>x" 
19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

50 
by (simp_all add: return_def fail_def cont_Abs_maybe Abs_maybe_inject) 
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

51 

e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

52 
lemma maybe_when_rews [simp]: 
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

53 
"maybe_when\<cdot>f\<cdot>r\<cdot>\<bottom> = \<bottom>" 
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

54 
"maybe_when\<cdot>f\<cdot>r\<cdot>fail = f" 
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

55 
"maybe_when\<cdot>f\<cdot>r\<cdot>(return\<cdot>x) = r\<cdot>x" 
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

56 
by (simp_all add: return_def fail_def maybe_when_def cont_Rep_maybe 
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

57 
cont_Abs_maybe Abs_maybe_inverse Rep_maybe_strict) 
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

58 

e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

59 
translations 
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

60 
"case m of fail \<Rightarrow> t1  return\<cdot>x \<Rightarrow> t2" == "maybe_when\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m" 
18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

61 

4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

62 

18097  63 
subsubsection {* Monadic bind operator *} 
16221  64 

18097  65 
constdefs 
66 
bind :: "'a maybe \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> 'b maybe" 

19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

67 
"bind \<equiv> \<Lambda> m f. case m of fail \<Rightarrow> fail  return\<cdot>x \<Rightarrow> f\<cdot>x" 
16221  68 

69 
text {* monad laws *} 

70 

19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

71 
lemma bind_strict [simp]: "bind\<cdot>\<bottom>\<cdot>f = \<bottom>" 
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

72 
by (simp add: bind_def) 
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

73 

e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

74 
lemma bind_fail [simp]: "bind\<cdot>fail\<cdot>f = fail" 
16221  75 
by (simp add: bind_def) 
76 

19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

77 
lemma left_unit [simp]: "bind\<cdot>(return\<cdot>a)\<cdot>k = k\<cdot>a" 
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

78 
by (simp add: bind_def) 
16221  79 

19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

80 
lemma right_unit [simp]: "bind\<cdot>m\<cdot>return = m" 
16221  81 
by (rule_tac p=m in maybeE, simp_all) 
82 

19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

83 
lemma bind_assoc: 
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

84 
"bind\<cdot>(bind\<cdot>m\<cdot>k)\<cdot>h = bind\<cdot>m\<cdot>(\<Lambda> a. bind\<cdot>(k\<cdot>a)\<cdot>h)" 
16221  85 
by (rule_tac p=m in maybeE, simp_all) 
86 

18097  87 
subsubsection {* Run operator *} 
16221  88 

89 
constdefs 

19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

90 
run:: "'a maybe \<rightarrow> 'a::pcpo" 
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

91 
"run \<equiv> maybe_when\<cdot>\<bottom>\<cdot>ID" 
16221  92 

93 
text {* rewrite rules for run *} 

94 

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

96 
by (simp add: run_def) 

97 

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

19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

99 
by (simp add: run_def) 
16221  100 

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

19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

102 
by (simp add: run_def) 
16221  103 

18097  104 
subsubsection {* Monad plus operator *} 
16221  105 

18097  106 
constdefs 
107 
mplus :: "'a maybe \<rightarrow> 'a maybe \<rightarrow> 'a maybe" 

19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

108 
"mplus \<equiv> \<Lambda> m1 m2. case m1 of fail \<Rightarrow> m2  return\<cdot>x \<Rightarrow> m1" 
18097  109 

110 
syntax "+++" :: "['a maybe, 'a maybe] \<Rightarrow> 'a maybe" (infixr "+++" 65) 

111 
translations "m1 +++ m2" == "mplus\<cdot>m1\<cdot>m2" 

16221  112 

113 
text {* rewrite rules for mplus *} 

114 

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

116 
by (simp add: mplus_def) 

117 

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

19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

119 
by (simp add: mplus_def) 
16221  120 

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

19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

122 
by (simp add: mplus_def) 
16221  123 

16460
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

124 
lemma mplus_fail2 [simp]: "m +++ fail = m" 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

125 
by (rule_tac p=m in maybeE, simp_all) 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

126 

16221  127 
lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)" 
128 
by (rule_tac p=x in maybeE, simp_all) 

129 

18097  130 
subsubsection {* Fatbar combinator *} 
131 

132 
constdefs 

133 
fatbar :: "('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe) \<rightarrow> ('a \<rightarrow> 'b maybe)" 

134 
"fatbar \<equiv> \<Lambda> a b x. a\<cdot>x +++ b\<cdot>x" 

135 

136 
syntax 

137 
"\<parallel>" :: "['a \<rightarrow> 'b maybe, 'a \<rightarrow> 'b maybe] \<Rightarrow> 'a \<rightarrow> 'b maybe" (infixr "\<parallel>" 60) 

138 
translations 

139 
"m1 \<parallel> m2" == "fatbar\<cdot>m1\<cdot>m2" 

140 

141 
lemma fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> (m \<parallel> ms)\<cdot>x = \<bottom>" 

142 
by (simp add: fatbar_def) 

143 

144 
lemma fatbar2: "m\<cdot>x = fail \<Longrightarrow> (m \<parallel> ms)\<cdot>x = ms\<cdot>x" 

145 
by (simp add: fatbar_def) 

146 

147 
lemma fatbar3: "m\<cdot>x = return\<cdot>y \<Longrightarrow> (m \<parallel> ms)\<cdot>x = return\<cdot>y" 

148 
by (simp add: fatbar_def) 

149 

150 
lemmas fatbar_simps = fatbar1 fatbar2 fatbar3 

151 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

152 
lemma run_fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = \<bottom>" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

153 
by (simp add: fatbar_def) 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

154 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

155 
lemma run_fatbar2: "m\<cdot>x = fail \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = run\<cdot>(ms\<cdot>x)" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

156 
by (simp add: fatbar_def) 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

157 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

158 
lemma run_fatbar3: "m\<cdot>x = return\<cdot>y \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = y" 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

159 
by (simp add: fatbar_def) 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

160 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

161 
lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

162 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

163 
subsection {* Case branch combinator *} 
18097  164 

165 
constdefs 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

166 
branch :: "('a \<rightarrow> 'b maybe) \<Rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'c maybe)" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

167 
"branch p \<equiv> \<Lambda> r x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> y. return\<cdot>(r\<cdot>y))" 
18097  168 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

169 
lemma branch_rews: 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

170 
"p\<cdot>x = \<bottom> \<Longrightarrow> branch p\<cdot>r\<cdot>x = \<bottom>" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

171 
"p\<cdot>x = fail \<Longrightarrow> branch p\<cdot>r\<cdot>x = fail" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

172 
"p\<cdot>x = return\<cdot>y \<Longrightarrow> branch p\<cdot>r\<cdot>x = return\<cdot>(r\<cdot>y)" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

173 
by (simp_all add: branch_def) 
18097  174 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

175 
lemma branch_return [simp]: "branch return\<cdot>r\<cdot>x = return\<cdot>(r\<cdot>x)" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

176 
by (simp add: branch_def) 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

177 

18097  178 

179 
subsection {* Case syntax *} 

180 

181 
nonterminals 

182 
Case_syn Cases_syn 

183 

184 
syntax 

185 
"_Case_syntax":: "['a, Cases_syn] => 'b" ("(Case _ of/ _)" 10) 

186 
"_Case1" :: "['a, 'b] => Case_syn" ("(2_ =>/ _)" 10) 

187 
"" :: "Case_syn => Cases_syn" ("_") 

188 
"_Case2" :: "[Case_syn, Cases_syn] => Cases_syn" ("_/  _") 

189 

190 
syntax (xsymbols) 

191 
"_Case1" :: "['a, 'b] => Case_syn" ("(2_ \<Rightarrow>/ _)" 10) 

192 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

193 
translations 
19439  194 
"_Case_syntax x ms" == "Fixrec.run\<cdot>(ms\<cdot>x)" 
18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

195 
"_Case2 m ms" == "m \<parallel> ms" 
18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

196 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

197 
text {* Parsing Case expressions *} 
18097  198 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

199 
syntax 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

200 
"_pat" :: "'a" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

201 
"_var" :: "'a" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

202 

18097  203 
translations 
18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

204 
"_Case1 p r" => "branch (_pat p)\<cdot>(_var p r)" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

205 
"_var (_args x y) r" => "csplit\<cdot>(_var x (_var y r))" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

206 
"_var () r" => "unit_when\<cdot>r" 
18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

207 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

208 
parse_translation {* 
18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

209 
(* rewrites (_pat x) => (return) *) 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

210 
(* rewrites (_var x t) => (Abs_CFun (%x. t)) *) 
19104  211 
[("_pat", K (Syntax.const "Fixrec.return")), 
18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

212 
mk_binder_tr ("_var", "Abs_CFun")]; 
18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

213 
*} 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

214 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

215 
text {* Printing Case expressions *} 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

216 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

217 
syntax 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

218 
"_match" :: "'a" 
18097  219 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

220 
print_translation {* 
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

221 
let 
18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

222 
fun dest_LAM (Const ("Rep_CFun",_) $ Const ("unit_when",_) $ t) = 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

223 
(Syntax.const "Unity", t) 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

224 
 dest_LAM (Const ("Rep_CFun",_) $ Const ("csplit",_) $ t) = 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

225 
let 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

226 
val (v1, t1) = dest_LAM t; 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

227 
val (v2, t2) = dest_LAM t1; 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

228 
in (Syntax.const "_args" $ v1 $ v2, t2) end 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

229 
 dest_LAM (Const ("Abs_CFun",_) $ t) = 
18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

230 
let 
18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

231 
val abs = case t of Abs abs => abs 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

232 
 _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0); 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

233 
val (x, t') = atomic_abs_tr' abs; 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

234 
in (Syntax.const "_var" $ x, t') end 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

235 
 dest_LAM _ = raise Match; (* too few vars: abort translation *) 
18097  236 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

237 
fun Case1_tr' [Const("branch",_) $ p, r] = 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

238 
let val (v, t) = dest_LAM r; 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

239 
in Syntax.const "_Case1" $ (Syntax.const "_match" $ p $ v) $ t end; 
18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

240 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

241 
in [("Rep_CFun", Case1_tr')] end; 
18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

242 
*} 
18097  243 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

244 
translations 
19104  245 
"x" <= "_match Fixrec.return (_var x)" 
18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

246 

4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

247 

4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

248 
subsection {* Pattern combinators for data constructors *} 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

249 

4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

250 
types ('a, 'b) pat = "'a \<rightarrow> 'b maybe" 
18097  251 

252 
constdefs 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

253 
cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat" 
19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

254 
"cpair_pat p1 p2 \<equiv> \<Lambda>\<langle>x, y\<rangle>. 
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

255 
bind\<cdot>(p1\<cdot>x)\<cdot>(\<Lambda> a. bind\<cdot>(p2\<cdot>y)\<cdot>(\<Lambda> b. return\<cdot>\<langle>a, b\<rangle>))" 
18097  256 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

257 
spair_pat :: 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

258 
"('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a::pcpo \<otimes> 'b::pcpo, 'c \<times> 'd) pat" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

259 
"spair_pat p1 p2 \<equiv> \<Lambda>(:x, y:). cpair_pat p1 p2\<cdot>\<langle>x, y\<rangle>" 
18097  260 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

261 
sinl_pat :: "('a, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

262 
"sinl_pat p \<equiv> sscase\<cdot>p\<cdot>(\<Lambda> x. fail)" 
18097  263 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

264 
sinr_pat :: "('b, 'c) pat \<Rightarrow> ('a::pcpo \<oplus> 'b::pcpo, 'c) pat" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

265 
"sinr_pat p \<equiv> sscase\<cdot>(\<Lambda> x. fail)\<cdot>p" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

266 

4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

267 
up_pat :: "('a, 'b) pat \<Rightarrow> ('a u, 'b) pat" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

268 
"up_pat p \<equiv> fup\<cdot>p" 
18097  269 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

270 
TT_pat :: "(tr, unit) pat" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

271 
"TT_pat \<equiv> \<Lambda> b. If b then return\<cdot>() else fail fi" 
18097  272 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

273 
FF_pat :: "(tr, unit) pat" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

274 
"FF_pat \<equiv> \<Lambda> b. If b then fail else return\<cdot>() fi" 
18097  275 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

276 
ONE_pat :: "(one, unit) pat" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

277 
"ONE_pat \<equiv> \<Lambda> ONE. return\<cdot>()" 
18097  278 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

279 
text {* Parse translations (patterns) *} 
18097  280 
translations 
18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

281 
"_pat (cpair\<cdot>x\<cdot>y)" => "cpair_pat (_pat x) (_pat y)" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

282 
"_pat (spair\<cdot>x\<cdot>y)" => "spair_pat (_pat x) (_pat y)" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

283 
"_pat (sinl\<cdot>x)" => "sinl_pat (_pat x)" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

284 
"_pat (sinr\<cdot>x)" => "sinr_pat (_pat x)" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

285 
"_pat (up\<cdot>x)" => "up_pat (_pat x)" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

286 
"_pat TT" => "TT_pat" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

287 
"_pat FF" => "FF_pat" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

288 
"_pat ONE" => "ONE_pat" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

289 

4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

290 
text {* Parse translations (variables) *} 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

291 
translations 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

292 
"_var (cpair\<cdot>x\<cdot>y) r" => "_var (_args x y) r" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

293 
"_var (spair\<cdot>x\<cdot>y) r" => "_var (_args x y) r" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

294 
"_var (sinl\<cdot>x) r" => "_var x r" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

295 
"_var (sinr\<cdot>x) r" => "_var x r" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

296 
"_var (up\<cdot>x) r" => "_var x r" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

297 
"_var TT r" => "_var () r" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

298 
"_var FF r" => "_var () r" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

299 
"_var ONE r" => "_var () r" 
18097  300 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

301 
text {* Print translations *} 
18097  302 
translations 
18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

303 
"cpair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

304 
<= "_match (cpair_pat p1 p2) (_args v1 v2)" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

305 
"spair\<cdot>(_match p1 v1)\<cdot>(_match p2 v2)" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

306 
<= "_match (spair_pat p1 p2) (_args v1 v2)" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

307 
"sinl\<cdot>(_match p1 v1)" <= "_match (sinl_pat p1) v1" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

308 
"sinr\<cdot>(_match p1 v1)" <= "_match (sinr_pat p1) v1" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

309 
"up\<cdot>(_match p1 v1)" <= "_match (up_pat p1) v1" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

310 
"TT" <= "_match TT_pat ()" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

311 
"FF" <= "_match FF_pat ()" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

312 
"ONE" <= "_match ONE_pat ()" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

313 

4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

314 
lemma cpair_pat1: 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

315 
"branch p\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = \<bottom>" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

316 
apply (simp add: branch_def cpair_pat_def) 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

317 
apply (rule_tac p="p\<cdot>x" in maybeE, simp_all) 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

318 
done 
18097  319 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

320 
lemma cpair_pat2: 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

321 
"branch p\<cdot>r\<cdot>x = fail \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = fail" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

322 
apply (simp add: branch_def cpair_pat_def) 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

323 
apply (rule_tac p="p\<cdot>x" in maybeE, simp_all) 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

324 
done 
18097  325 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

326 
lemma cpair_pat3: 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

327 
"branch p\<cdot>r\<cdot>x = return\<cdot>s \<Longrightarrow> 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

328 
branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = branch q\<cdot>s\<cdot>y" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

329 
apply (simp add: branch_def cpair_pat_def) 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

330 
apply (rule_tac p="p\<cdot>x" in maybeE, simp_all) 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

331 
apply (rule_tac p="q\<cdot>y" in maybeE, simp_all) 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

332 
done 
18097  333 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

334 
lemmas cpair_pat [simp] = 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

335 
cpair_pat1 cpair_pat2 cpair_pat3 
18097  336 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

337 
lemma spair_pat [simp]: 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

338 
"branch (spair_pat p1 p2)\<cdot>r\<cdot>\<bottom> = \<bottom>" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

339 
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

340 
\<Longrightarrow> branch (spair_pat p1 p2)\<cdot>r\<cdot>(:x, y:) = 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

341 
branch (cpair_pat p1 p2)\<cdot>r\<cdot>\<langle>x, y\<rangle>" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

342 
by (simp_all add: branch_def spair_pat_def) 
18097  343 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

344 
lemma sinl_pat [simp]: 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

345 
"branch (sinl_pat p)\<cdot>r\<cdot>\<bottom> = \<bottom>" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

346 
"x \<noteq> \<bottom> \<Longrightarrow> branch (sinl_pat p)\<cdot>r\<cdot>(sinl\<cdot>x) = branch p\<cdot>r\<cdot>x" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

347 
"y \<noteq> \<bottom> \<Longrightarrow> branch (sinl_pat p)\<cdot>r\<cdot>(sinr\<cdot>y) = fail" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

348 
by (simp_all add: branch_def sinl_pat_def) 
18097  349 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

350 
lemma sinr_pat [simp]: 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

351 
"branch (sinr_pat p)\<cdot>r\<cdot>\<bottom> = \<bottom>" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

352 
"x \<noteq> \<bottom> \<Longrightarrow> branch (sinr_pat p)\<cdot>r\<cdot>(sinl\<cdot>x) = fail" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

353 
"y \<noteq> \<bottom> \<Longrightarrow> branch (sinr_pat p)\<cdot>r\<cdot>(sinr\<cdot>y) = branch p\<cdot>r\<cdot>y" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

354 
by (simp_all add: branch_def sinr_pat_def) 
18097  355 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

356 
lemma up_pat [simp]: 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

357 
"branch (up_pat p)\<cdot>r\<cdot>\<bottom> = \<bottom>" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

358 
"branch (up_pat p)\<cdot>r\<cdot>(up\<cdot>x) = branch p\<cdot>r\<cdot>x" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

359 
by (simp_all add: branch_def up_pat_def) 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

360 

4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

361 
lemma TT_pat [simp]: 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

362 
"branch TT_pat\<cdot>(unit_when\<cdot>r)\<cdot>\<bottom> = \<bottom>" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

363 
"branch TT_pat\<cdot>(unit_when\<cdot>r)\<cdot>TT = return\<cdot>r" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

364 
"branch TT_pat\<cdot>(unit_when\<cdot>r)\<cdot>FF = fail" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

365 
by (simp_all add: branch_def TT_pat_def) 
18097  366 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

367 
lemma FF_pat [simp]: 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

368 
"branch FF_pat\<cdot>(unit_when\<cdot>r)\<cdot>\<bottom> = \<bottom>" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

369 
"branch FF_pat\<cdot>(unit_when\<cdot>r)\<cdot>TT = fail" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

370 
"branch FF_pat\<cdot>(unit_when\<cdot>r)\<cdot>FF = return\<cdot>r" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

371 
by (simp_all add: branch_def FF_pat_def) 
18097  372 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

373 
lemma ONE_pat [simp]: 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

374 
"branch ONE_pat\<cdot>(unit_when\<cdot>r)\<cdot>\<bottom> = \<bottom>" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

375 
"branch ONE_pat\<cdot>(unit_when\<cdot>r)\<cdot>ONE = return\<cdot>r" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

376 
by (simp_all add: branch_def ONE_pat_def) 
18097  377 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

378 

4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

379 
subsection {* Wildcards, aspatterns, and lazy patterns *} 
18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

380 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

381 
syntax 
18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

382 
"_as_pat" :: "[idt, 'a] \<Rightarrow> 'a" (infixr "\<as>" 10) 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

383 
"_lazy_pat" :: "'a \<Rightarrow> 'a" ("\<lazy> _" [1000] 1000) 
18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

384 

dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

385 
constdefs 
18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

386 
wild_pat :: "'a \<rightarrow> unit maybe" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

387 
"wild_pat \<equiv> \<Lambda> x. return\<cdot>()" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

388 

4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

389 
as_pat :: "('a \<rightarrow> 'b maybe) \<Rightarrow> 'a \<rightarrow> ('a \<times> 'b) maybe" 
19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

390 
"as_pat p \<equiv> \<Lambda> x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> a. return\<cdot>\<langle>x, a\<rangle>)" 
18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

391 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

392 
lazy_pat :: "('a \<rightarrow> 'b::pcpo maybe) \<Rightarrow> ('a \<rightarrow> 'b maybe)" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

393 
"lazy_pat p \<equiv> \<Lambda> x. return\<cdot>(run\<cdot>(p\<cdot>x))" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

394 

4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

395 
text {* Parse translations (patterns) *} 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

396 
translations 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

397 
"_pat _" => "wild_pat" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

398 
"_pat (_as_pat x y)" => "as_pat (_pat y)" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

399 
"_pat (_lazy_pat x)" => "lazy_pat (_pat x)" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

400 

4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

401 
text {* Parse translations (variables) *} 
18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

402 
translations 
18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

403 
"_var _ r" => "_var () r" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

404 
"_var (_as_pat x y) r" => "_var (_args x y) r" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

405 
"_var (_lazy_pat x) r" => "_var x r" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

406 

4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

407 
text {* Print translations *} 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

408 
translations 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

409 
"_" <= "_match wild_pat ()" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

410 
"_as_pat x (_match p v)" <= "_match (as_pat p) (_args (_var x) v)" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

411 
"_lazy_pat (_match p v)" <= "_match (lazy_pat p) v" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

412 

19327  413 
text {* Lazy patterns in lambda abstractions *} 
414 
translations 

415 
"_cabs (_lazy_pat p) r" == "run oo (_Case1 (_lazy_pat p) r)" 

416 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

417 
lemma wild_pat [simp]: "branch wild_pat\<cdot>(unit_when\<cdot>r)\<cdot>x = return\<cdot>r" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

418 
by (simp add: branch_def wild_pat_def) 
18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

419 

18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

420 
lemma as_pat [simp]: 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

421 
"branch (as_pat p)\<cdot>(csplit\<cdot>r)\<cdot>x = branch p\<cdot>(r\<cdot>x)\<cdot>x" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

422 
apply (simp add: branch_def as_pat_def) 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

423 
apply (rule_tac p="p\<cdot>x" in maybeE, simp_all) 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

424 
done 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

425 

4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

426 
lemma lazy_pat [simp]: 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

427 
"branch p\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> branch (lazy_pat p)\<cdot>r\<cdot>x = return\<cdot>(r\<cdot>\<bottom>)" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

428 
"branch p\<cdot>r\<cdot>x = fail \<Longrightarrow> branch (lazy_pat p)\<cdot>r\<cdot>x = return\<cdot>(r\<cdot>\<bottom>)" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

429 
"branch p\<cdot>r\<cdot>x = return\<cdot>s \<Longrightarrow> branch (lazy_pat p)\<cdot>r\<cdot>x = return\<cdot>s" 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

430 
apply (simp_all add: branch_def lazy_pat_def) 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

431 
apply (rule_tac [!] p="p\<cdot>x" in maybeE, simp_all) 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

432 
done 
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

433 

18112
dc1d6f588204
reimplemented Case syntax using print/parse translations; moved aspatterns to separate section
huffman
parents:
18110
diff
changeset

434 

16221  435 
subsection {* Match functions for builtin types *} 
436 

16776
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

437 
defaultsort pcpo 
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

438 

16221  439 
constdefs 
16776
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

440 
match_UU :: "'a \<rightarrow> unit maybe" 
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

441 
"match_UU \<equiv> \<Lambda> x. fail" 
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

442 

a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

443 
match_cpair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<times> 'b) maybe" 
16221  444 
"match_cpair \<equiv> csplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)" 
445 

16551  446 
match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<times> 'b) maybe" 
447 
"match_spair \<equiv> ssplit\<cdot>(\<Lambda> x y. return\<cdot><x,y>)" 

448 

449 
match_sinl :: "'a \<oplus> 'b \<rightarrow> 'a maybe" 

450 
"match_sinl \<equiv> sscase\<cdot>return\<cdot>(\<Lambda> y. fail)" 

451 

452 
match_sinr :: "'a \<oplus> 'b \<rightarrow> 'b maybe" 

453 
"match_sinr \<equiv> sscase\<cdot>(\<Lambda> x. fail)\<cdot>return" 

454 

16776
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

455 
match_up :: "'a::cpo u \<rightarrow> 'a maybe" 
16221  456 
"match_up \<equiv> fup\<cdot>return" 
457 

16460
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

458 
match_ONE :: "one \<rightarrow> unit maybe" 
18094  459 
"match_ONE \<equiv> \<Lambda> ONE. return\<cdot>()" 
460 

16460
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

461 
match_TT :: "tr \<rightarrow> unit maybe" 
18094  462 
"match_TT \<equiv> \<Lambda> b. If b then return\<cdot>() else fail fi" 
463 

16460
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

464 
match_FF :: "tr \<rightarrow> unit maybe" 
18094  465 
"match_FF \<equiv> \<Lambda> b. If b then fail else return\<cdot>() fi" 
16460
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

466 

16776
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

467 
lemma match_UU_simps [simp]: 
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

468 
"match_UU\<cdot>x = fail" 
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

469 
by (simp add: match_UU_def) 
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

470 

16221  471 
lemma match_cpair_simps [simp]: 
472 
"match_cpair\<cdot><x,y> = return\<cdot><x,y>" 

473 
by (simp add: match_cpair_def) 

474 

16551  475 
lemma match_spair_simps [simp]: 
476 
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> match_spair\<cdot>(:x,y:) = return\<cdot><x,y>" 

477 
"match_spair\<cdot>\<bottom> = \<bottom>" 

478 
by (simp_all add: match_spair_def) 

479 

480 
lemma match_sinl_simps [simp]: 

481 
"x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinl\<cdot>x) = return\<cdot>x" 

482 
"x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinr\<cdot>x) = fail" 

483 
"match_sinl\<cdot>\<bottom> = \<bottom>" 

484 
by (simp_all add: match_sinl_def) 

485 

486 
lemma match_sinr_simps [simp]: 

487 
"x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinr\<cdot>x) = return\<cdot>x" 

488 
"x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinl\<cdot>x) = fail" 

489 
"match_sinr\<cdot>\<bottom> = \<bottom>" 

490 
by (simp_all add: match_sinr_def) 

491 

16221  492 
lemma match_up_simps [simp]: 
493 
"match_up\<cdot>(up\<cdot>x) = return\<cdot>x" 

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

495 
by (simp_all add: match_up_def) 

496 

16460
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

497 
lemma match_ONE_simps [simp]: 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

498 
"match_ONE\<cdot>ONE = return\<cdot>()" 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

499 
"match_ONE\<cdot>\<bottom> = \<bottom>" 
18094  500 
by (simp_all add: match_ONE_def) 
16460
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

501 

72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

502 
lemma match_TT_simps [simp]: 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

503 
"match_TT\<cdot>TT = return\<cdot>()" 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

504 
"match_TT\<cdot>FF = fail" 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

505 
"match_TT\<cdot>\<bottom> = \<bottom>" 
18094  506 
by (simp_all add: match_TT_def) 
16460
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

507 

72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

508 
lemma match_FF_simps [simp]: 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

509 
"match_FF\<cdot>FF = return\<cdot>()" 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

510 
"match_FF\<cdot>TT = fail" 
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

511 
"match_FF\<cdot>\<bottom> = \<bottom>" 
18094  512 
by (simp_all add: match_FF_def) 
16460
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

513 

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

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

515 

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

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

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

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

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

520 

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

521 
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

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

523 

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

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

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

526 

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

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

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

529 

16463
342d74ca8815
fixrec shows unsolved subgoals when proofs of rewrites fail
huffman
parents:
16460
diff
changeset

530 
text {* lemma for proving rewrite rules *} 
342d74ca8815
fixrec shows unsolved subgoals when proofs of rewrites fail
huffman
parents:
16460
diff
changeset

531 

342d74ca8815
fixrec shows unsolved subgoals when proofs of rewrites fail
huffman
parents:
16460
diff
changeset

532 
lemma ssubst_lhs: "\<lbrakk>t = s; P s = Q\<rbrakk> \<Longrightarrow> P t = Q" 
342d74ca8815
fixrec shows unsolved subgoals when proofs of rewrites fail
huffman
parents:
16460
diff
changeset

533 
by simp 
342d74ca8815
fixrec shows unsolved subgoals when proofs of rewrites fail
huffman
parents:
16460
diff
changeset

534 

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

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

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

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

538 
val cpair_eqD2 = thm "cpair_eqD2"; 
16463
342d74ca8815
fixrec shows unsolved subgoals when proofs of rewrites fail
huffman
parents:
16460
diff
changeset

539 
val ssubst_lhs = thm "ssubst_lhs"; 
18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

540 
val branch_def = thm "branch_def"; 
16401
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

541 
*} 
16221  542 

16758  543 
subsection {* Initializing the fixrec package *} 
16221  544 

23152  545 
use "Tools/fixrec_package.ML" 
16221  546 

19439  547 
hide (open) const return bind fail run 
19104  548 

16221  549 
end 