author  huffman 
Wed, 10 Nov 2010 17:56:08 0800  
changeset 40502  8e92772bc0e8 
parent 40327  1dfdbd66093a 
child 40735  6f65843e78f3 
permissions  rwrr 
16221  1 
(* Title: HOLCF/Fixrec.thy 
2 
Author: Amber Telfer and Brian Huffman 

3 
*) 

4 

5 
header "Package for defining recursive functions in HOLCF" 

6 

7 
theory Fixrec 

40502
8e92772bc0e8
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
40327
diff
changeset

8 
imports Plain_HOLCF 
35527  9 
uses 
10 
("Tools/holcf_library.ML") 

11 
("Tools/fixrec.ML") 

16221  12 
begin 
13 

37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

14 
subsection {* Patternmatch monad *} 
16221  15 

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

17 

37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

18 
pcpodef (open) 'a match = "UNIV::(one ++ 'a u) set" 
29063
7619f0561cd7
pcpodef package: state two goals, instead of encoded conjunction;
wenzelm
parents:
28891
diff
changeset

19 
by simp_all 
16221  20 

29141  21 
definition 
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

22 
fail :: "'a match" where 
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

23 
"fail = Abs_match (sinl\<cdot>ONE)" 
16221  24 

29141  25 
definition 
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

26 
succeed :: "'a \<rightarrow> 'a match" where 
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

27 
"succeed = (\<Lambda> x. Abs_match (sinr\<cdot>(up\<cdot>x)))" 
19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

28 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
23152
diff
changeset

29 
definition 
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

30 
match_case :: "'b \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a match \<rightarrow> 'b::pcpo" where 
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

31 
"match_case = (\<Lambda> f r m. sscase\<cdot>(\<Lambda> x. f)\<cdot>(fup\<cdot>r)\<cdot>(Rep_match m))" 
16221  32 

37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

33 
lemma matchE [case_names bottom fail succeed, cases type: match]: 
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

34 
"\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = fail \<Longrightarrow> Q; \<And>x. p = succeed\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" 
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

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

36 
apply (cases p, rename_tac r) 
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

37 
apply (rule_tac p=r in ssumE, simp add: Abs_match_strict) 
16221  38 
apply (rule_tac p=x in oneE, simp, simp) 
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

39 
apply (rule_tac p=y in upE, simp, simp add: cont_Abs_match) 
16221  40 
done 
41 

37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

42 
lemma succeed_defined [simp]: "succeed\<cdot>x \<noteq> \<bottom>" 
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

43 
by (simp add: succeed_def cont_Abs_match Abs_match_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 fail_defined [simp]: "fail \<noteq> \<bottom>" 
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

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

47 

37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

48 
lemma succeed_eq [simp]: "(succeed\<cdot>x = succeed\<cdot>y) = (x = y)" 
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

49 
by (simp add: succeed_def cont_Abs_match Abs_match_inject) 
18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

50 

37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

51 
lemma succeed_neq_fail [simp]: 
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

52 
"succeed\<cdot>x \<noteq> fail" "fail \<noteq> succeed\<cdot>x" 
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

53 
by (simp_all add: succeed_def fail_def cont_Abs_match Abs_match_inject) 
19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

54 

37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

55 
lemma match_case_simps [simp]: 
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

56 
"match_case\<cdot>f\<cdot>r\<cdot>\<bottom> = \<bottom>" 
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

57 
"match_case\<cdot>f\<cdot>r\<cdot>fail = f" 
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

58 
"match_case\<cdot>f\<cdot>r\<cdot>(succeed\<cdot>x) = r\<cdot>x" 
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

59 
by (simp_all add: succeed_def fail_def match_case_def cont_Rep_match 
29530
9905b660612b
change to simpler, more extensible continuity simproc
huffman
parents:
29322
diff
changeset

60 
cont2cont_LAM 
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

61 
cont_Abs_match Abs_match_inverse Rep_match_strict) 
19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

62 

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

63 
translations 
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

64 
"case m of XCONST fail \<Rightarrow> t1  XCONST succeed\<cdot>x \<Rightarrow> t2" 
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

65 
== "CONST match_case\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m" 
18293
4eaa654c92f2
reimplement Case expression pattern matching to support lazy patterns
huffman
parents:
18112
diff
changeset

66 

18097  67 
subsubsection {* Run operator *} 
16221  68 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
23152
diff
changeset

69 
definition 
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

70 
run :: "'a match \<rightarrow> 'a::pcpo" where 
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

71 
"run = match_case\<cdot>\<bottom>\<cdot>ID" 
16221  72 

73 
text {* rewrite rules for run *} 

74 

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

76 
by (simp add: run_def) 

77 

78 
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

79 
by (simp add: run_def) 
16221  80 

37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

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

82 
by (simp add: run_def) 
16221  83 

18097  84 
subsubsection {* Monad plus operator *} 
16221  85 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
23152
diff
changeset

86 
definition 
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

87 
mplus :: "'a match \<rightarrow> 'a match \<rightarrow> 'a match" where 
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

88 
"mplus = (\<Lambda> m1 m2. case m1 of fail \<Rightarrow> m2  succeed\<cdot>x \<Rightarrow> m1)" 
18097  89 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
23152
diff
changeset

90 
abbreviation 
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

91 
mplus_syn :: "['a match, 'a match] \<Rightarrow> 'a match" (infixr "+++" 65) where 
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
23152
diff
changeset

92 
"m1 +++ m2 == mplus\<cdot>m1\<cdot>m2" 
16221  93 

94 
text {* rewrite rules for mplus *} 

95 

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

97 
by (simp add: mplus_def) 

98 

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

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

100 
by (simp add: mplus_def) 
16221  101 

37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

102 
lemma mplus_succeed [simp]: "succeed\<cdot>x +++ m = succeed\<cdot>x" 
19092
e32cf29f01fc
make maybe into a real type constructor; remove monad syntax
huffman
parents:
18293
diff
changeset

103 
by (simp add: mplus_def) 
16221  104 

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

105 
lemma mplus_fail2 [simp]: "m +++ fail = m" 
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

106 
by (cases m, simp_all) 
16460
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

107 

16221  108 
lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)" 
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

109 
by (cases x, simp_all) 
16221  110 

111 
subsection {* Match functions for builtin types *} 

112 

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

114 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
23152
diff
changeset

115 
definition 
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

116 
match_UU :: "'a \<rightarrow> 'c match \<rightarrow> 'c match" 
30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

117 
where 
40046
ba2e41c8b725
introduce function strict :: 'a > 'b > 'b, which works like Haskell's seq; use strict instead of strictify in various definitions
huffman
parents:
39807
diff
changeset

118 
"match_UU = (\<Lambda> x k. strict\<cdot>x\<cdot>fail)" 
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
23152
diff
changeset

119 

2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
23152
diff
changeset

120 
definition 
39807  121 
match_Pair :: "'a::cpo \<times> 'b::cpo \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match" 
30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

122 
where 
39807  123 
"match_Pair = (\<Lambda> x k. csplit\<cdot>k\<cdot>x)" 
16776
a3899ac14a1c
generalized types of monadic operators to class cpo; added match function for UU
huffman
parents:
16758
diff
changeset

124 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
23152
diff
changeset

125 
definition 
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

126 
match_spair :: "'a \<otimes> 'b \<rightarrow> ('a \<rightarrow> 'b \<rightarrow> 'c match) \<rightarrow> 'c match" 
30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

127 
where 
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

128 
"match_spair = (\<Lambda> x k. ssplit\<cdot>k\<cdot>x)" 
16221  129 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
23152
diff
changeset

130 
definition 
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

131 
match_sinl :: "'a \<oplus> 'b \<rightarrow> ('a \<rightarrow> 'c match) \<rightarrow> 'c match" 
30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

132 
where 
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

133 
"match_sinl = (\<Lambda> x k. sscase\<cdot>k\<cdot>(\<Lambda> b. fail)\<cdot>x)" 
16551  134 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
23152
diff
changeset

135 
definition 
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

136 
match_sinr :: "'a \<oplus> 'b \<rightarrow> ('b \<rightarrow> 'c match) \<rightarrow> 'c match" 
30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

137 
where 
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

138 
"match_sinr = (\<Lambda> x k. sscase\<cdot>(\<Lambda> a. fail)\<cdot>k\<cdot>x)" 
16551  139 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
23152
diff
changeset

140 
definition 
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

141 
match_up :: "'a::cpo u \<rightarrow> ('a \<rightarrow> 'c match) \<rightarrow> 'c match" 
30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

142 
where 
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

143 
"match_up = (\<Lambda> x k. fup\<cdot>k\<cdot>x)" 
16221  144 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
23152
diff
changeset

145 
definition 
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

146 
match_ONE :: "one \<rightarrow> 'c match \<rightarrow> 'c match" 
30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

147 
where 
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

148 
"match_ONE = (\<Lambda> ONE k. k)" 
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

149 

4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

150 
definition 
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

151 
match_TT :: "tr \<rightarrow> 'c match \<rightarrow> 'c match" 
30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

152 
where 
40322
707eb30e8a53
make syntax of continuous ifthenelse consistent with HOL ifthenelse
huffman
parents:
40046
diff
changeset

153 
"match_TT = (\<Lambda> x k. If x then k else fail)" 
18094  154 

25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
23152
diff
changeset

155 
definition 
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

156 
match_FF :: "tr \<rightarrow> 'c match \<rightarrow> 'c match" 
30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

157 
where 
40322
707eb30e8a53
make syntax of continuous ifthenelse consistent with HOL ifthenelse
huffman
parents:
40046
diff
changeset

158 
"match_FF = (\<Lambda> x k. If x then fail else k)" 
16460
72a08d509d62
added match functions for ONE, TT, and FF; added theorem mplus_fail2
huffman
parents:
16417
diff
changeset

159 

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

160 
lemma match_UU_simps [simp]: 
31008
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30914
diff
changeset

161 
"match_UU\<cdot>\<bottom>\<cdot>k = \<bottom>" 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30914
diff
changeset

162 
"x \<noteq> \<bottom> \<Longrightarrow> match_UU\<cdot>x\<cdot>k = fail" 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30914
diff
changeset

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

164 

39807  165 
lemma match_Pair_simps [simp]: 
166 
"match_Pair\<cdot>(x, y)\<cdot>k = k\<cdot>x\<cdot>y" 

167 
by (simp_all add: match_Pair_def) 

16221  168 

16551  169 
lemma match_spair_simps [simp]: 
30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

170 
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> match_spair\<cdot>(:x, y:)\<cdot>k = k\<cdot>x\<cdot>y" 
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

171 
"match_spair\<cdot>\<bottom>\<cdot>k = \<bottom>" 
16551  172 
by (simp_all add: match_spair_def) 
173 

174 
lemma match_sinl_simps [simp]: 

30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

175 
"x \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinl\<cdot>x)\<cdot>k = k\<cdot>x" 
30914
ceeb5f2eac75
fix toospecific types in lemmas match_{sinl,sinr}_simps
huffman
parents:
30912
diff
changeset

176 
"y \<noteq> \<bottom> \<Longrightarrow> match_sinl\<cdot>(sinr\<cdot>y)\<cdot>k = fail" 
30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

177 
"match_sinl\<cdot>\<bottom>\<cdot>k = \<bottom>" 
16551  178 
by (simp_all add: match_sinl_def) 
179 

180 
lemma match_sinr_simps [simp]: 

30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

181 
"x \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinl\<cdot>x)\<cdot>k = fail" 
30914
ceeb5f2eac75
fix toospecific types in lemmas match_{sinl,sinr}_simps
huffman
parents:
30912
diff
changeset

182 
"y \<noteq> \<bottom> \<Longrightarrow> match_sinr\<cdot>(sinr\<cdot>y)\<cdot>k = k\<cdot>y" 
30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

183 
"match_sinr\<cdot>\<bottom>\<cdot>k = \<bottom>" 
16551  184 
by (simp_all add: match_sinr_def) 
185 

16221  186 
lemma match_up_simps [simp]: 
30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

187 
"match_up\<cdot>(up\<cdot>x)\<cdot>k = k\<cdot>x" 
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

188 
"match_up\<cdot>\<bottom>\<cdot>k = \<bottom>" 
16221  189 
by (simp_all add: match_up_def) 
190 

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

191 
lemma match_ONE_simps [simp]: 
30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

192 
"match_ONE\<cdot>ONE\<cdot>k = k" 
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

193 
"match_ONE\<cdot>\<bottom>\<cdot>k = \<bottom>" 
18094  194 
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

195 

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

196 
lemma match_TT_simps [simp]: 
30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

197 
"match_TT\<cdot>TT\<cdot>k = k" 
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

198 
"match_TT\<cdot>FF\<cdot>k = fail" 
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

199 
"match_TT\<cdot>\<bottom>\<cdot>k = \<bottom>" 
18094  200 
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

201 

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

202 
lemma match_FF_simps [simp]: 
30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

203 
"match_FF\<cdot>FF\<cdot>k = k" 
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

204 
"match_FF\<cdot>TT\<cdot>k = fail" 
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30131
diff
changeset

205 
"match_FF\<cdot>\<bottom>\<cdot>k = \<bottom>" 
18094  206 
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

207 

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

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

209 

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

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

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

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

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

214 

31095
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31008
diff
changeset

215 
lemma Pair_equalI: "\<lbrakk>x \<equiv> fst p; y \<equiv> snd p\<rbrakk> \<Longrightarrow> (x, y) \<equiv> p" 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31008
diff
changeset

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

217 

31095
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31008
diff
changeset

218 
lemma Pair_eqD1: "(x, y) = (x', y') \<Longrightarrow> x = x'" 
16401
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

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

220 

31095
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31008
diff
changeset

221 
lemma Pair_eqD2: "(x, y) = (x', y') \<Longrightarrow> y = y'" 
16401
57c35ede00b9
fixrec package now handles mutuallyrecursive definitions
huffman
parents:
16229
diff
changeset

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

223 

31095
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31008
diff
changeset

224 
lemma def_cont_fix_eq: 
40327  225 
"\<lbrakk>f \<equiv> fix\<cdot>(Abs_cfun F); cont F\<rbrakk> \<Longrightarrow> f = F f" 
31095
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31008
diff
changeset

226 
by (simp, subst fix_eq, simp) 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31008
diff
changeset

227 

b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31008
diff
changeset

228 
lemma def_cont_fix_ind: 
40327  229 
"\<lbrakk>f \<equiv> fix\<cdot>(Abs_cfun F); cont F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F x)\<rbrakk> \<Longrightarrow> P f" 
31095
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31008
diff
changeset

230 
by (simp add: fix_ind) 
b79d140f6d0b
simplify fixrec proofs for mutuallyrecursive definitions; generate better fixpoint induction rules
huffman
parents:
31008
diff
changeset

231 

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

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

233 

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

234 
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

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

236 

16221  237 

16758  238 
subsection {* Initializing the fixrec package *} 
16221  239 

35527  240 
use "Tools/holcf_library.ML" 
31738
7b9b9ba532ca
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31095
diff
changeset

241 
use "Tools/fixrec.ML" 
16221  242 

31738
7b9b9ba532ca
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31095
diff
changeset

243 
setup {* Fixrec.setup *} 
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29530
diff
changeset

244 

6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29530
diff
changeset

245 
setup {* 
31738
7b9b9ba532ca
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31095
diff
changeset

246 
Fixrec.add_matchers 
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29530
diff
changeset

247 
[ (@{const_name up}, @{const_name match_up}), 
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29530
diff
changeset

248 
(@{const_name sinl}, @{const_name match_sinl}), 
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29530
diff
changeset

249 
(@{const_name sinr}, @{const_name match_sinr}), 
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29530
diff
changeset

250 
(@{const_name spair}, @{const_name match_spair}), 
39807  251 
(@{const_name Pair}, @{const_name match_Pair}), 
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29530
diff
changeset

252 
(@{const_name ONE}, @{const_name match_ONE}), 
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29530
diff
changeset

253 
(@{const_name TT}, @{const_name match_TT}), 
31008
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30914
diff
changeset

254 
(@{const_name FF}, @{const_name match_FF}), 
b8f4e351b5bf
add proper support for bottompatterns in fixrec package
huffman
parents:
30914
diff
changeset

255 
(@{const_name UU}, @{const_name match_UU}) ] 
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29530
diff
changeset

256 
*} 
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29530
diff
changeset

257 

37109
e67760c1b851
move unused pattern match syntax stuff into HOLCF/ex
huffman
parents:
37108
diff
changeset

258 
hide_const (open) succeed fail run 
19104  259 

16221  260 
end 