author | wenzelm |
Tue, 29 Mar 2011 17:47:11 +0200 | |
changeset 42151 | 4da4fc77664b |
parent 41296 | 6aaf80ea9715 |
child 42361 | 23f352990944 |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Tools/fixrec.ML |
23152 | 2 |
Author: Amber Telfer and Brian Huffman |
3 |
||
4 |
Recursive function definition package for HOLCF. |
|
5 |
*) |
|
6 |
||
31738
7b9b9ba532ca
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset
|
7 |
signature FIXREC = |
23152 | 8 |
sig |
40041
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
40036
diff
changeset
|
9 |
val add_fixrec: (binding * typ option * mixfix) list |
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
40036
diff
changeset
|
10 |
-> (bool * (Attrib.binding * term)) list -> local_theory -> local_theory |
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
40036
diff
changeset
|
11 |
val add_fixrec_cmd: (binding * string option * mixfix) list |
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
40036
diff
changeset
|
12 |
-> (bool * (Attrib.binding * string)) list -> local_theory -> local_theory |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
13 |
val add_matchers: (string * string) list -> theory -> theory |
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
14 |
val fixrec_simp_tac: Proof.context -> int -> tactic |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
15 |
val setup: theory -> theory |
40832 | 16 |
end |
23152 | 17 |
|
41296
6aaf80ea9715
switch to transparent ascription, to avoid warning messages
huffman
parents:
40832
diff
changeset
|
18 |
structure Fixrec : FIXREC = |
23152 | 19 |
struct |
20 |
||
40832 | 21 |
open HOLCF_Library |
35527 | 22 |
|
40832 | 23 |
infixr 6 ->> |
24 |
infix -->> |
|
25 |
infix 9 ` |
|
35527 | 26 |
|
40832 | 27 |
val def_cont_fix_eq = @{thm def_cont_fix_eq} |
28 |
val def_cont_fix_ind = @{thm def_cont_fix_ind} |
|
23152 | 29 |
|
40832 | 30 |
fun fixrec_err s = error ("fixrec definition error:\n" ^ s) |
23152 | 31 |
fun fixrec_eq_err thy s eq = |
40832 | 32 |
fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq)) |
23152 | 33 |
|
30132 | 34 |
(*************************************************************************) |
35 |
(***************************** building types ****************************) |
|
36 |
(*************************************************************************) |
|
37 |
||
33401
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
38 |
local |
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
39 |
|
35525 | 40 |
fun binder_cfun (Type(@{type_name cfun},[T, U])) = T :: binder_cfun U |
33401
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
41 |
| binder_cfun (Type(@{type_name "fun"},[T, U])) = T :: binder_cfun U |
40832 | 42 |
| binder_cfun _ = [] |
33401
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
43 |
|
35525 | 44 |
fun body_cfun (Type(@{type_name cfun},[T, U])) = body_cfun U |
33401
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
45 |
| body_cfun (Type(@{type_name "fun"},[T, U])) = body_cfun U |
40832 | 46 |
| body_cfun T = T |
33401
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
47 |
|
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
48 |
fun strip_cfun T : typ list * typ = |
40832 | 49 |
(binder_cfun T, body_cfun T) |
33401
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
50 |
|
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
51 |
in |
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
52 |
|
35527 | 53 |
fun matcherT (T, U) = |
40832 | 54 |
body_cfun T ->> (binder_cfun T -->> U) ->> U |
30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30485
diff
changeset
|
55 |
|
33401
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
56 |
end |
30132 | 57 |
|
58 |
(*************************************************************************) |
|
59 |
(***************************** building terms ****************************) |
|
60 |
(*************************************************************************) |
|
23152 | 61 |
|
40832 | 62 |
val mk_trp = HOLogic.mk_Trueprop |
23152 | 63 |
|
64 |
(* splits a cterm into the right and lefthand sides of equality *) |
|
40832 | 65 |
fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t) |
23152 | 66 |
|
67 |
(* similar to Thm.head_of, but for continuous application *) |
|
40327 | 68 |
fun chead_of (Const(@{const_name Rep_cfun},_)$f$t) = chead_of f |
40832 | 69 |
| chead_of u = u |
23152 | 70 |
|
40832 | 71 |
infix 0 == val (op ==) = Logic.mk_equals |
72 |
infix 1 === val (op ===) = HOLogic.mk_eq |
|
30132 | 73 |
|
74 |
fun mk_mplus (t, u) = |
|
75 |
let val mT = Term.fastype_of t |
|
40832 | 76 |
in Const(@{const_name Fixrec.mplus}, mT ->> mT ->> mT) ` t ` u end |
30132 | 77 |
|
78 |
fun mk_run t = |
|
37097
476016cbf8b3
for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run
huffman
parents:
37096
diff
changeset
|
79 |
let |
476016cbf8b3
for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run
huffman
parents:
37096
diff
changeset
|
80 |
val mT = Term.fastype_of t |
476016cbf8b3
for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run
huffman
parents:
37096
diff
changeset
|
81 |
val T = dest_matchT mT |
476016cbf8b3
for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run
huffman
parents:
37096
diff
changeset
|
82 |
val run = Const(@{const_name Fixrec.run}, mT ->> T) |
476016cbf8b3
for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run
huffman
parents:
37096
diff
changeset
|
83 |
in |
476016cbf8b3
for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run
huffman
parents:
37096
diff
changeset
|
84 |
case t of |
40327 | 85 |
Const(@{const_name Rep_cfun}, _) $ |
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37097
diff
changeset
|
86 |
Const(@{const_name Fixrec.succeed}, _) $ u => u |
37097
476016cbf8b3
for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run
huffman
parents:
37096
diff
changeset
|
87 |
| _ => run ` t |
40832 | 88 |
end |
30132 | 89 |
|
31095
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset
|
90 |
|
23152 | 91 |
(*************************************************************************) |
92 |
(************* fixed-point definitions and unfolding theorems ************) |
|
93 |
(*************************************************************************) |
|
94 |
||
33519 | 95 |
structure FixrecUnfoldData = Generic_Data |
96 |
( |
|
40832 | 97 |
type T = thm Symtab.table |
98 |
val empty = Symtab.empty |
|
99 |
val extend = I |
|
100 |
fun merge data : T = Symtab.merge (K true) data |
|
101 |
) |
|
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
102 |
|
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
103 |
local |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
104 |
|
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
105 |
fun name_of (Const (n, T)) = n |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
106 |
| name_of (Free (n, T)) = n |
40832 | 107 |
| name_of t = raise TERM ("Fixrec.add_unfold: lhs not a constant", [t]) |
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
108 |
|
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
109 |
val lhs_name = |
40832 | 110 |
name_of o head_of o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of |
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
111 |
|
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
112 |
in |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
113 |
|
33442 | 114 |
val add_unfold : attribute = |
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
115 |
Thm.declaration_attribute |
40832 | 116 |
(fn th => FixrecUnfoldData.map (Symtab.insert (K true) (lhs_name th, th))) |
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
117 |
|
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
118 |
end |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
119 |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
120 |
fun add_fixdefs |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
121 |
(fixes : ((binding * typ) * mixfix) list) |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
122 |
(spec : (Attrib.binding * term) list) |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
123 |
(lthy : local_theory) = |
23152 | 124 |
let |
40832 | 125 |
val thy = ProofContext.theory_of lthy |
126 |
val names = map (Binding.name_of o fst o fst) fixes |
|
127 |
val all_names = space_implode "_" names |
|
128 |
val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec) |
|
129 |
val functional = lambda_tuple lhss (mk_tuple rhss) |
|
130 |
val fixpoint = mk_fix (mk_cabs functional) |
|
36996
63fadc0a33db
more informative error message for fixrec when continuity proof fails
huffman
parents:
36960
diff
changeset
|
131 |
|
31095
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset
|
132 |
val cont_thm = |
36996
63fadc0a33db
more informative error message for fixrec when continuity proof fails
huffman
parents:
36960
diff
changeset
|
133 |
let |
40832 | 134 |
val prop = mk_trp (mk_cont functional) |
37096 | 135 |
fun err _ = error ( |
40832 | 136 |
"Continuity proof failed please check that cont2cont rules\n" ^ |
37097
476016cbf8b3
for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run
huffman
parents:
37096
diff
changeset
|
137 |
"or simp rules are configured for all non-HOLCF constants.\n" ^ |
36996
63fadc0a33db
more informative error message for fixrec when continuity proof fails
huffman
parents:
36960
diff
changeset
|
138 |
"The error occurred for the goal statement:\n" ^ |
40832 | 139 |
Syntax.string_of_term lthy prop) |
140 |
val rules = Cont2ContData.get lthy |
|
141 |
val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules)) |
|
142 |
val slow_tac = SOLVED' (simp_tac (simpset_of lthy)) |
|
143 |
val tac = fast_tac 1 ORELSE slow_tac 1 ORELSE err |
|
36996
63fadc0a33db
more informative error message for fixrec when continuity proof fails
huffman
parents:
36960
diff
changeset
|
144 |
in |
63fadc0a33db
more informative error message for fixrec when continuity proof fails
huffman
parents:
36960
diff
changeset
|
145 |
Goal.prove lthy [] [] prop (K tac) |
40832 | 146 |
end |
31095
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset
|
147 |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
148 |
fun one_def (l as Free(n,_)) r = |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset
|
149 |
let val b = Long_Name.base_name n |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
150 |
in ((Binding.name (b^"_def"), []), r) end |
40832 | 151 |
| one_def _ _ = fixrec_err "fixdefs: lhs not of correct form" |
23152 | 152 |
fun defs [] _ = [] |
153 |
| defs (l::[]) r = [one_def l r] |
|
40832 | 154 |
| defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r) |
155 |
val fixdefs = defs lhss fixpoint |
|
35772 | 156 |
val (fixdef_thms : (term * (string * thm)) list, lthy) = lthy |
40832 | 157 |
|> fold_map Local_Theory.define (map (apfst fst) fixes ~~ fixdefs) |
158 |
fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2] |
|
159 |
val tuple_fixdef_thm = foldr1 pair_equalI (map (snd o snd) fixdef_thms) |
|
160 |
val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT) |
|
161 |
val predicate = lambda_tuple lhss (list_comb (P, lhss)) |
|
31095
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset
|
162 |
val tuple_induct_thm = (def_cont_fix_ind OF [tuple_fixdef_thm, cont_thm]) |
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset
|
163 |
|> Drule.instantiate' [] [SOME (Thm.cterm_of thy predicate)] |
40832 | 164 |
|> Local_Defs.unfold lthy @{thms split_paired_all split_conv split_strict} |
31095
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset
|
165 |
val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm]) |
40832 | 166 |
|> Local_Defs.unfold lthy @{thms split_conv} |
23152 | 167 |
fun unfolds [] thm = [] |
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
168 |
| unfolds (n::[]) thm = [(n, thm)] |
23152 | 169 |
| unfolds (n::ns) thm = let |
40832 | 170 |
val thmL = thm RS @{thm Pair_eqD1} |
171 |
val thmR = thm RS @{thm Pair_eqD2} |
|
172 |
in (n, thmL) :: unfolds ns thmR end |
|
173 |
val unfold_thms = unfolds names tuple_unfold_thm |
|
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
174 |
val induct_note : Attrib.binding * Thm.thm list = |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
175 |
let |
40832 | 176 |
val thm_name = Binding.qualify true all_names (Binding.name "induct") |
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
177 |
in |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
178 |
((thm_name, []), [tuple_induct_thm]) |
40832 | 179 |
end |
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
180 |
fun unfold_note (name, thm) : Attrib.binding * Thm.thm list = |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
181 |
let |
40832 | 182 |
val thm_name = Binding.qualify true name (Binding.name "unfold") |
183 |
val src = Attrib.internal (K add_unfold) |
|
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
184 |
in |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
185 |
((thm_name, [src]), [thm]) |
40832 | 186 |
end |
35772 | 187 |
val (thmss, lthy) = lthy |
40832 | 188 |
|> fold_map Local_Theory.note (induct_note :: map unfold_note unfold_thms) |
23152 | 189 |
in |
35772 | 190 |
(lthy, names, fixdef_thms, map snd unfold_thms) |
40832 | 191 |
end |
23152 | 192 |
|
193 |
(*************************************************************************) |
|
194 |
(*********** monadic notation and pattern matching compilation ***********) |
|
195 |
(*************************************************************************) |
|
196 |
||
33522 | 197 |
structure FixrecMatchData = Theory_Data |
198 |
( |
|
40832 | 199 |
type T = string Symtab.table |
200 |
val empty = Symtab.empty |
|
201 |
val extend = I |
|
202 |
fun merge data = Symtab.merge (K true) data |
|
203 |
) |
|
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
204 |
|
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
205 |
(* associate match functions with pattern constants *) |
40832 | 206 |
fun add_matchers ms = FixrecMatchData.map (fold Symtab.update ms) |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
207 |
|
30157 | 208 |
fun taken_names (t : term) : bstring list = |
209 |
let |
|
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset
|
210 |
fun taken (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs |
30157 | 211 |
| taken (Free(a,_) , bs) = insert (op =) a bs |
212 |
| taken (f $ u , bs) = taken (f, taken (u, bs)) |
|
213 |
| taken (Abs(a,_,t), bs) = taken (t, insert (op =) a bs) |
|
40832 | 214 |
| taken (_ , bs) = bs |
30157 | 215 |
in |
216 |
taken (t, []) |
|
40832 | 217 |
end |
23152 | 218 |
|
39805 | 219 |
(* builds a monadic term for matching a pattern *) |
220 |
(* returns (rhs, free variable, used varnames) *) |
|
221 |
fun compile_pat match_name pat rhs taken = |
|
222 |
let |
|
223 |
fun comp_pat p rhs taken = |
|
224 |
if is_Free p then (rhs, p, taken) |
|
225 |
else comp_con (fastype_of p) p rhs [] taken |
|
226 |
(* compiles a monadic term for a constructor pattern *) |
|
227 |
and comp_con T p rhs vs taken = |
|
228 |
case p of |
|
40327 | 229 |
Const(@{const_name Rep_cfun},_) $ f $ x => |
39805 | 230 |
let val (rhs', v, taken') = comp_pat x rhs taken |
231 |
in comp_con T f rhs' (v::vs) taken' end |
|
232 |
| f $ x => |
|
233 |
let val (rhs', v, taken') = comp_pat x rhs taken |
|
234 |
in comp_con T f rhs' (v::vs) taken' end |
|
235 |
| Const (c, cT) => |
|
236 |
let |
|
237 |
val n = Name.variant taken "v" |
|
238 |
val v = Free(n, T) |
|
239 |
val m = Const(match_name c, matcherT (cT, fastype_of rhs)) |
|
240 |
val k = big_lambdas vs rhs |
|
241 |
in |
|
242 |
(m`v`k, v, n::taken) |
|
243 |
end |
|
244 |
| _ => raise TERM ("fixrec: invalid pattern ", [p]) |
|
245 |
in |
|
246 |
comp_pat pat rhs taken |
|
40832 | 247 |
end |
23152 | 248 |
|
249 |
(* builds a monadic term for matching a function definition pattern *) |
|
40036 | 250 |
(* returns (constant, (vars, matcher)) *) |
39804
b1cec1fcd95f
rename some fixrec pattern-match compilation functions
huffman
parents:
39557
diff
changeset
|
251 |
fun compile_lhs match_name pat rhs vs taken = |
23152 | 252 |
case pat of |
40327 | 253 |
Const(@{const_name Rep_cfun}, _) $ f $ x => |
40832 | 254 |
let val (rhs', v, taken') = compile_pat match_name x rhs taken |
39804
b1cec1fcd95f
rename some fixrec pattern-match compilation functions
huffman
parents:
39557
diff
changeset
|
255 |
in compile_lhs match_name f rhs' (v::vs) taken' end |
40036 | 256 |
| Free(_,_) => (pat, (vs, rhs)) |
257 |
| Const(_,_) => (pat, (vs, rhs)) |
|
258 |
| _ => fixrec_err ("invalid function pattern: " |
|
40832 | 259 |
^ ML_Syntax.print_term pat) |
23152 | 260 |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
261 |
fun strip_alls t = |
40832 | 262 |
if Logic.is_all t then strip_alls (snd (Logic.dest_all t)) else t |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
263 |
|
39804
b1cec1fcd95f
rename some fixrec pattern-match compilation functions
huffman
parents:
39557
diff
changeset
|
264 |
fun compile_eq match_name eq = |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
265 |
let |
40832 | 266 |
val (lhs,rhs) = dest_eqs (Logic.strip_imp_concl (strip_alls eq)) |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
267 |
in |
39804
b1cec1fcd95f
rename some fixrec pattern-match compilation functions
huffman
parents:
39557
diff
changeset
|
268 |
compile_lhs match_name lhs (mk_succeed rhs) [] (taken_names eq) |
40832 | 269 |
end |
23152 | 270 |
|
271 |
(* this is the pattern-matching compiler function *) |
|
39804
b1cec1fcd95f
rename some fixrec pattern-match compilation functions
huffman
parents:
39557
diff
changeset
|
272 |
fun compile_eqs match_name eqs = |
23152 | 273 |
let |
40036 | 274 |
val (consts, matchers) = |
40832 | 275 |
ListPair.unzip (map (compile_eq match_name) eqs) |
40036 | 276 |
val const = |
277 |
case distinct (op =) consts of |
|
35903 | 278 |
[n] => n |
40832 | 279 |
| _ => fixrec_err "all equations in block must define the same function" |
40036 | 280 |
val vars = |
281 |
case distinct (op = o pairself length) (map fst matchers) of |
|
282 |
[vars] => vars |
|
40832 | 283 |
| _ => fixrec_err "all equations in block must have the same arity" |
40036 | 284 |
(* rename so all matchers use same free variables *) |
40832 | 285 |
fun rename (vs, t) = Term.subst_free (filter_out (op =) (vs ~~ vars)) t |
286 |
val rhs = big_lambdas vars (mk_run (foldr1 mk_mplus (map rename matchers))) |
|
23152 | 287 |
in |
40036 | 288 |
mk_trp (const === rhs) |
40832 | 289 |
end |
23152 | 290 |
|
291 |
(*************************************************************************) |
|
292 |
(********************** Proving associated theorems **********************) |
|
293 |
(*************************************************************************) |
|
294 |
||
40832 | 295 |
fun eta_tac i = CONVERSION Thm.eta_conversion i |
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
296 |
|
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
297 |
fun fixrec_simp_tac ctxt = |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
298 |
let |
40832 | 299 |
val tab = FixrecUnfoldData.get (Context.Proof ctxt) |
300 |
val ss = Simplifier.simpset_of ctxt |
|
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
301 |
fun concl t = |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
302 |
if Logic.is_all t then concl (snd (Logic.dest_all t)) |
40832 | 303 |
else HOLogic.dest_Trueprop (Logic.strip_imp_concl t) |
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
304 |
fun tac (t, i) = |
33430 | 305 |
let |
35903 | 306 |
val (c, T) = |
40832 | 307 |
(dest_Const o head_of o chead_of o fst o HOLogic.dest_eq o concl) t |
308 |
val unfold_thm = the (Symtab.lookup tab c) |
|
309 |
val rule = unfold_thm RS @{thm ssubst_lhs} |
|
33430 | 310 |
in |
37081 | 311 |
CHANGED (rtac rule i THEN eta_tac i THEN asm_simp_tac ss i) |
33430 | 312 |
end |
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
313 |
in |
33505 | 314 |
SUBGOAL (fn ti => the_default no_tac (try tac ti)) |
40832 | 315 |
end |
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
316 |
|
23152 | 317 |
(* proves a block of pattern matching equations as theorems, using unfold *) |
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
wenzelm
parents:
31740
diff
changeset
|
318 |
fun make_simps ctxt (unfold_thm, eqns : (Attrib.binding * term) list) = |
23152 | 319 |
let |
40832 | 320 |
val ss = Simplifier.simpset_of ctxt |
321 |
val rule = unfold_thm RS @{thm ssubst_lhs} |
|
322 |
val tac = rtac rule 1 THEN eta_tac 1 THEN asm_simp_tac ss 1 |
|
323 |
fun prove_term t = Goal.prove ctxt [] [] t (K tac) |
|
324 |
fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t) |
|
23152 | 325 |
in |
326 |
map prove_eqn eqns |
|
40832 | 327 |
end |
23152 | 328 |
|
329 |
(*************************************************************************) |
|
330 |
(************************* Main fixrec function **************************) |
|
331 |
(*************************************************************************) |
|
332 |
||
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
333 |
local |
31738
7b9b9ba532ca
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset
|
334 |
(* code adapted from HOL/Tools/primrec.ML *) |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
335 |
|
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
336 |
fun gen_fixrec |
30485 | 337 |
prep_spec |
40041
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
40036
diff
changeset
|
338 |
(raw_fixes : (binding * 'a option * mixfix) list) |
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
40036
diff
changeset
|
339 |
(raw_spec' : (bool * (Attrib.binding * 'b)) list) |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
340 |
(lthy : local_theory) = |
23152 | 341 |
let |
40832 | 342 |
val (skips, raw_spec) = ListPair.unzip raw_spec' |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
343 |
val (fixes : ((binding * typ) * mixfix) list, |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
344 |
spec : (Attrib.binding * term) list) = |
40832 | 345 |
fst (prep_spec raw_fixes raw_spec lthy) |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
346 |
val chead_of_spec = |
40832 | 347 |
chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
348 |
fun name_of (Free (n, _)) = n |
40832 | 349 |
| name_of t = fixrec_err ("unknown term") |
350 |
val all_names = map (name_of o chead_of_spec) spec |
|
351 |
val names = distinct (op =) all_names |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
352 |
fun block_of_name n = |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
353 |
map_filter |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
354 |
(fn (m,eq) => if m = n then SOME eq else NONE) |
40832 | 355 |
(all_names ~~ (spec ~~ skips)) |
356 |
val blocks = map block_of_name names |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
357 |
|
40832 | 358 |
val matcher_tab = FixrecMatchData.get (ProofContext.theory_of lthy) |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
359 |
fun match_name c = |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
360 |
case Symtab.lookup matcher_tab c of SOME m => m |
40832 | 361 |
| NONE => fixrec_err ("unknown pattern constructor: " ^ c) |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
362 |
|
40832 | 363 |
val matches = map (compile_eqs match_name) (map (map (snd o fst)) blocks) |
364 |
val spec' = map (pair Attrib.empty_binding) matches |
|
35772 | 365 |
val (lthy, cnames, fixdef_thms, unfold_thms) = |
40832 | 366 |
add_fixdefs fixes spec' lthy |
40041
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
40036
diff
changeset
|
367 |
|
40832 | 368 |
val blocks' = map (map fst o filter_out snd) blocks |
40041
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
40036
diff
changeset
|
369 |
val simps : (Attrib.binding * thm) list list = |
40832 | 370 |
map (make_simps lthy) (unfold_thms ~~ blocks') |
40041
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
40036
diff
changeset
|
371 |
fun mk_bind n : Attrib.binding = |
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
40036
diff
changeset
|
372 |
(Binding.qualify true n (Binding.name "simps"), |
40832 | 373 |
[Attrib.internal (K Simplifier.simp_add)]) |
40041
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
40036
diff
changeset
|
374 |
val simps1 : (Attrib.binding * thm list) list = |
40832 | 375 |
map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps) |
40041
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
40036
diff
changeset
|
376 |
val simps2 : (Attrib.binding * thm list) list = |
40832 | 377 |
map (apsnd (fn thm => [thm])) (flat simps) |
40041
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
40036
diff
changeset
|
378 |
val (_, lthy) = lthy |
40832 | 379 |
|> fold_map Local_Theory.note (simps1 @ simps2) |
23152 | 380 |
in |
40041
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
40036
diff
changeset
|
381 |
lthy |
40832 | 382 |
end |
23152 | 383 |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
384 |
in |
23152 | 385 |
|
40832 | 386 |
val add_fixrec = gen_fixrec Specification.check_spec |
387 |
val add_fixrec_cmd = gen_fixrec Specification.read_spec |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
388 |
|
40832 | 389 |
end (* local *) |
23152 | 390 |
|
391 |
||
392 |
(*************************************************************************) |
|
393 |
(******************************** Parsers ********************************) |
|
394 |
(*************************************************************************) |
|
395 |
||
40096
4d1a8fa8cdfd
change fixrec parser to not accept theorem names with (unchecked) option
huffman
parents:
40041
diff
changeset
|
396 |
val opt_thm_name' : (bool * Attrib.binding) parser = |
4d1a8fa8cdfd
change fixrec parser to not accept theorem names with (unchecked) option
huffman
parents:
40041
diff
changeset
|
397 |
Parse.$$$ "(" -- Parse.$$$ "unchecked" -- Parse.$$$ ")" >> K (true, Attrib.empty_binding) |
40832 | 398 |
|| Parse_Spec.opt_thm_name ":" >> pair false |
40096
4d1a8fa8cdfd
change fixrec parser to not accept theorem names with (unchecked) option
huffman
parents:
40041
diff
changeset
|
399 |
|
4d1a8fa8cdfd
change fixrec parser to not accept theorem names with (unchecked) option
huffman
parents:
40041
diff
changeset
|
400 |
val spec' : (bool * (Attrib.binding * string)) parser = |
40832 | 401 |
opt_thm_name' -- Parse.prop >> (fn ((a, b), c) => (a, (b, c))) |
40096
4d1a8fa8cdfd
change fixrec parser to not accept theorem names with (unchecked) option
huffman
parents:
40041
diff
changeset
|
402 |
|
40041
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
40036
diff
changeset
|
403 |
val alt_specs' : (bool * (Attrib.binding * string)) list parser = |
40832 | 404 |
let val unexpected = Scan.ahead (Parse.name || Parse.$$$ "[" || Parse.$$$ "(") |
405 |
in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! (Parse.$$$ "|"))) end |
|
40041
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
40036
diff
changeset
|
406 |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
407 |
val _ = |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
408 |
Outer_Syntax.local_theory "fixrec" "define recursive functions (HOLCF)" Keyword.thy_decl |
40041
1f09b4c7b85e
replace fixrec 'permissive' mode with per-equation 'unchecked' option
huffman
parents:
40036
diff
changeset
|
409 |
(Parse.fixes -- (Parse.where_ |-- Parse.!!! alt_specs') |
40832 | 410 |
>> (fn (fixes, specs) => add_fixrec_cmd fixes specs)) |
23152 | 411 |
|
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
412 |
val setup = |
37080
a2a1c8a658ef
remove fixrec_simp attribute; fixrec uses default simpset from theory context instead
huffman
parents:
37079
diff
changeset
|
413 |
Method.setup @{binding fixrec_simp} |
a2a1c8a658ef
remove fixrec_simp attribute; fixrec uses default simpset from theory context instead
huffman
parents:
37079
diff
changeset
|
414 |
(Scan.succeed (SIMPLE_METHOD' o fixrec_simp_tac)) |
40832 | 415 |
"pattern prover for fixrec constants" |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
416 |
|
40832 | 417 |
end |