author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46950  d0181abdbdac 
child 47432  e1576d13e933 
permissions  rwrr 
42151  1 
(* Title: HOL/HOLCF/Fixrec.thy 
16221  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 
46950
d0181abdbdac
declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents:
42151
diff
changeset

9 
keywords "fixrec" :: thy_decl 
35527  10 
uses 
11 
("Tools/holcf_library.ML") 

12 
("Tools/fixrec.ML") 

16221  13 
begin 
14 

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

15 
subsection {* Patternmatch monad *} 
16221  16 

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

18 

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

19 
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

20 
by simp_all 
16221  21 

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

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

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

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

27 
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

28 
"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

29 

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

30 
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

31 
"\<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

32 
unfolding fail_def succeed_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) 
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37080
diff
changeset

34 
apply (rule_tac p=r in ssumE, simp add: Abs_match_strict) 
16221  35 
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

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

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

39 
lemma succeed_defined [simp]: "succeed\<cdot>x \<noteq> \<bottom>" 
41029
f7d8cfa6e7fc
pcpodef no longer generates _defined lemmas, use _bottom_iff lemmas instead
huffman
parents:
40834
diff
changeset

40 
by (simp add: succeed_def cont_Abs_match Abs_match_bottom_iff) 
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>" 
41029
f7d8cfa6e7fc
pcpodef no longer generates _defined lemmas, use _bottom_iff lemmas instead
huffman
parents:
40834
diff
changeset

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

44 

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

45 
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

46 
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

47 

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

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

49 
"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

50 
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

51 

18097  52 
subsubsection {* Run operator *} 
16221  53 

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

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

55 
run :: "'a match \<rightarrow> 'a::pcpo" where 
40735  56 
"run = (\<Lambda> m. sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)\<cdot>(Rep_match m))" 
16221  57 

58 
text {* rewrite rules for run *} 

59 

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

40735  61 
unfolding run_def 
62 
by (simp add: cont_Rep_match Rep_match_strict) 

16221  63 

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

40735  65 
unfolding run_def fail_def 
66 
by (simp add: cont_Rep_match Abs_match_inverse) 

16221  67 

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

68 
lemma run_succeed [simp]: "run\<cdot>(succeed\<cdot>x) = x" 
40735  69 
unfolding run_def succeed_def 
70 
by (simp add: cont_Rep_match cont_Abs_match Abs_match_inverse) 

16221  71 

18097  72 
subsubsection {* Monad plus operator *} 
16221  73 

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

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

75 
mplus :: "'a match \<rightarrow> 'a match \<rightarrow> 'a match" where 
40735  76 
"mplus = (\<Lambda> m1 m2. sscase\<cdot>(\<Lambda> _. m2)\<cdot>(\<Lambda> _. m1)\<cdot>(Rep_match m1))" 
18097  77 

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

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

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

80 
"m1 +++ m2 == mplus\<cdot>m1\<cdot>m2" 
16221  81 

82 
text {* rewrite rules for mplus *} 

83 

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

40735  85 
unfolding mplus_def 
40834
a1249aeff5b6
change cpodefgenerated cont_Rep rules to cont2cont format
huffman
parents:
40795
diff
changeset

86 
by (simp add: cont_Rep_match Rep_match_strict) 
16221  87 

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

40735  89 
unfolding mplus_def fail_def 
40834
a1249aeff5b6
change cpodefgenerated cont_Rep rules to cont2cont format
huffman
parents:
40795
diff
changeset

90 
by (simp add: cont_Rep_match Abs_match_inverse) 
16221  91 

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

92 
lemma mplus_succeed [simp]: "succeed\<cdot>x +++ m = succeed\<cdot>x" 
40735  93 
unfolding mplus_def succeed_def 
40834
a1249aeff5b6
change cpodefgenerated cont_Rep rules to cont2cont format
huffman
parents:
40795
diff
changeset

94 
by (simp add: cont_Rep_match cont_Abs_match Abs_match_inverse) 
16221  95 

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

96 
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

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

98 

16221  99 
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

100 
by (cases x, simp_all) 
16221  101 

102 
subsection {* Match functions for builtin types *} 

103 

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

105 

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

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

108 
where 
40768  109 
"match_bottom = (\<Lambda> x k. seq\<cdot>x\<cdot>fail)" 
25131
2c8caac48ade
modernized specifications ('definition', 'abbreviation', 'notation');
wenzelm
parents:
23152
diff
changeset

110 

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

111 
definition 
39807  112 
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

113 
where 
39807  114 
"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

115 

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

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

117 
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

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

119 
"match_spair = (\<Lambda> x k. ssplit\<cdot>k\<cdot>x)" 
16221  120 

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

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

122 
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

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

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

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

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

127 
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

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

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

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

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

132 
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

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

134 
"match_up = (\<Lambda> x k. fup\<cdot>k\<cdot>x)" 
16221  135 

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

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

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

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

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

140 

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

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

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

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

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

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

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

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

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

149 
"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

150 

40768  151 
lemma match_bottom_simps [simp]: 
40795
c52cd8bc426d
change match_bottom_simps to produce ifthenelse, making more uses of bottompatterns work with fixrec
huffman
parents:
40774
diff
changeset

152 
"match_bottom\<cdot>x\<cdot>k = (if x = \<bottom> then \<bottom> else fail)" 
c52cd8bc426d
change match_bottom_simps to produce ifthenelse, making more uses of bottompatterns work with fixrec
huffman
parents:
40774
diff
changeset

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

154 

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

157 
by (simp_all add: match_Pair_def) 

16221  158 

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

160 
"\<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

161 
"match_spair\<cdot>\<bottom>\<cdot>k = \<bottom>" 
16551  162 
by (simp_all add: match_spair_def) 
163 

164 
lemma match_sinl_simps [simp]: 

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

165 
"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

166 
"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

167 
"match_sinl\<cdot>\<bottom>\<cdot>k = \<bottom>" 
16551  168 
by (simp_all add: match_sinl_def) 
169 

170 
lemma match_sinr_simps [simp]: 

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

171 
"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

172 
"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

173 
"match_sinr\<cdot>\<bottom>\<cdot>k = \<bottom>" 
16551  174 
by (simp_all add: match_sinr_def) 
175 

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

177 
"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

178 
"match_up\<cdot>\<bottom>\<cdot>k = \<bottom>" 
16221  179 
by (simp_all add: match_up_def) 
180 

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

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

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

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

185 

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

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

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

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

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

191 

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

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

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

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

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

197 

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

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

199 

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

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

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

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

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

204 

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

205 
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

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

207 

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

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

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

210 

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

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

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

213 

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

214 
lemma def_cont_fix_eq: 
40327  215 
"\<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

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

217 

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

218 
lemma def_cont_fix_ind: 
40327  219 
"\<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

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

221 

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

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

223 

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

224 
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

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

226 

16221  227 

16758  228 
subsection {* Initializing the fixrec package *} 
16221  229 

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

231 
use "Tools/fixrec.ML" 
16221  232 

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

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

234 

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

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

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

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

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

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

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

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

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

244 
(@{const_name FF}, @{const_name match_FF}), 
41429
cf5f025bc3c7
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
huffman
parents:
41029
diff
changeset

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

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

247 

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

248 
hide_const (open) succeed fail run 
19104  249 

16221  250 
end 