author | wenzelm |
Thu, 15 Mar 2012 22:08:53 +0100 | |
changeset 46950 | d0181abdbdac |
parent 42151 | 4da4fc77664b |
child 47432 | e1576d13e933 |
permissions | -rw-r--r-- |
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 {* Pattern-match 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 cpodef-generated 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 cpodef-generated 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 cpodef-generated 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 built-in 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 if-then-else consistent with HOL if-then-else
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 if-then-else consistent with HOL if-then-else
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 if-then-else, making more uses of bottom-patterns 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 if-then-else, making more uses of bottom-patterns 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 too-specific 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 too-specific 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 mutually-recursive definitions
huffman
parents:
16229
diff
changeset
|
198 |
subsection {* Mutual recursion *} |
57c35ede00b9
fixrec package now handles mutually-recursive definitions
huffman
parents:
16229
diff
changeset
|
199 |
|
57c35ede00b9
fixrec package now handles mutually-recursive definitions
huffman
parents:
16229
diff
changeset
|
200 |
text {* |
57c35ede00b9
fixrec package now handles mutually-recursive definitions
huffman
parents:
16229
diff
changeset
|
201 |
The following rules are used to prove unfolding theorems from |
57c35ede00b9
fixrec package now handles mutually-recursive definitions
huffman
parents:
16229
diff
changeset
|
202 |
fixed-point definitions of mutually recursive functions. |
57c35ede00b9
fixrec package now handles mutually-recursive definitions
huffman
parents:
16229
diff
changeset
|
203 |
*} |
57c35ede00b9
fixrec package now handles mutually-recursive definitions
huffman
parents:
16229
diff
changeset
|
204 |
|
31095
b79d140f6d0b
simplify fixrec proofs for mutually-recursive 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 mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31008
diff
changeset
|
206 |
by simp |
16401
57c35ede00b9
fixrec package now handles mutually-recursive definitions
huffman
parents:
16229
diff
changeset
|
207 |
|
31095
b79d140f6d0b
simplify fixrec proofs for mutually-recursive 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 mutually-recursive definitions
huffman
parents:
16229
diff
changeset
|
209 |
by simp |
57c35ede00b9
fixrec package now handles mutually-recursive definitions
huffman
parents:
16229
diff
changeset
|
210 |
|
31095
b79d140f6d0b
simplify fixrec proofs for mutually-recursive 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 mutually-recursive definitions
huffman
parents:
16229
diff
changeset
|
212 |
by simp |
57c35ede00b9
fixrec package now handles mutually-recursive definitions
huffman
parents:
16229
diff
changeset
|
213 |
|
31095
b79d140f6d0b
simplify fixrec proofs for mutually-recursive 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 mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31008
diff
changeset
|
216 |
by (simp, subst fix_eq, simp) |
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31008
diff
changeset
|
217 |
|
b79d140f6d0b
simplify fixrec proofs for mutually-recursive 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 mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31008
diff
changeset
|
220 |
by (simp add: fix_ind) |
b79d140f6d0b
simplify fixrec proofs for mutually-recursive 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 bottom-patterns 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 |