author | huffman |
Mon, 24 May 2010 09:32:52 -0700 | |
changeset 37108 | 00f13d3ad474 |
parent 37097 | 476016cbf8b3 |
child 39557 | fe5722fce758 |
permissions | -rw-r--r-- |
31738
7b9b9ba532ca
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset
|
1 |
(* Title: 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 |
30485 | 9 |
val add_fixrec: bool -> (binding * typ option * mixfix) list |
10 |
-> (Attrib.binding * term) list -> local_theory -> local_theory |
|
11 |
val add_fixrec_cmd: bool -> (binding * string option * mixfix) list |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
12 |
-> (Attrib.binding * string) list -> local_theory -> local_theory |
30485 | 13 |
val add_fixpat: Thm.binding * term list -> theory -> theory |
14 |
val add_fixpat_cmd: Attrib.binding * string list -> theory -> theory |
|
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
15 |
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
|
16 |
val fixrec_simp_tac: Proof.context -> int -> tactic |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
17 |
val setup: theory -> theory |
23152 | 18 |
end; |
19 |
||
31738
7b9b9ba532ca
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset
|
20 |
structure Fixrec :> FIXREC = |
23152 | 21 |
struct |
22 |
||
35527 | 23 |
open HOLCF_Library; |
24 |
||
25 |
infixr 6 ->>; |
|
26 |
infix -->>; |
|
27 |
infix 9 `; |
|
28 |
||
31095
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset
|
29 |
val def_cont_fix_eq = @{thm def_cont_fix_eq}; |
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset
|
30 |
val def_cont_fix_ind = @{thm def_cont_fix_ind}; |
23152 | 31 |
|
32 |
fun fixrec_err s = error ("fixrec definition error:\n" ^ s); |
|
33 |
fun fixrec_eq_err thy s eq = |
|
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26343
diff
changeset
|
34 |
fixrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq)); |
23152 | 35 |
|
30132 | 36 |
(*************************************************************************) |
37 |
(***************************** building types ****************************) |
|
38 |
(*************************************************************************) |
|
39 |
||
33401
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
40 |
local |
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
41 |
|
35525 | 42 |
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
|
43 |
| binder_cfun (Type(@{type_name "fun"},[T, U])) = T :: binder_cfun U |
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
44 |
| binder_cfun _ = []; |
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
45 |
|
35525 | 46 |
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
|
47 |
| body_cfun (Type(@{type_name "fun"},[T, U])) = body_cfun U |
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
48 |
| body_cfun T = T; |
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
49 |
|
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
50 |
fun strip_cfun T : typ list * typ = |
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
51 |
(binder_cfun T, body_cfun T); |
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
52 |
|
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
53 |
in |
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
54 |
|
35527 | 55 |
fun matcherT (T, U) = |
56 |
body_cfun T ->> (binder_cfun T -->> U) ->> U; |
|
30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30485
diff
changeset
|
57 |
|
33401
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
58 |
end |
30132 | 59 |
|
60 |
(*************************************************************************) |
|
61 |
(***************************** building terms ****************************) |
|
62 |
(*************************************************************************) |
|
23152 | 63 |
|
64 |
val mk_trp = HOLogic.mk_Trueprop; |
|
65 |
||
66 |
(* splits a cterm into the right and lefthand sides of equality *) |
|
67 |
fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t); |
|
68 |
||
69 |
(* similar to Thm.head_of, but for continuous application *) |
|
26045 | 70 |
fun chead_of (Const(@{const_name Rep_CFun},_)$f$t) = chead_of f |
23152 | 71 |
| chead_of u = u; |
72 |
||
30132 | 73 |
infix 0 ==; val (op ==) = Logic.mk_equals; |
74 |
infix 1 ===; val (op ===) = HOLogic.mk_eq; |
|
75 |
||
76 |
fun mk_mplus (t, u) = |
|
77 |
let val mT = Term.fastype_of t |
|
78 |
in Const(@{const_name Fixrec.mplus}, mT ->> mT ->> mT) ` t ` u end; |
|
79 |
||
80 |
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
|
81 |
let |
476016cbf8b3
for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run
huffman
parents:
37096
diff
changeset
|
82 |
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
|
83 |
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
|
84 |
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
|
85 |
in |
476016cbf8b3
for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run
huffman
parents:
37096
diff
changeset
|
86 |
case t of |
476016cbf8b3
for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run
huffman
parents:
37096
diff
changeset
|
87 |
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
|
88 |
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
|
89 |
| _ => run ` t |
476016cbf8b3
for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run
huffman
parents:
37096
diff
changeset
|
90 |
end; |
30132 | 91 |
|
31095
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset
|
92 |
|
23152 | 93 |
(*************************************************************************) |
94 |
(************* fixed-point definitions and unfolding theorems ************) |
|
95 |
(*************************************************************************) |
|
96 |
||
33519 | 97 |
structure FixrecUnfoldData = Generic_Data |
98 |
( |
|
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
99 |
type T = thm Symtab.table; |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
100 |
val empty = Symtab.empty; |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
101 |
val extend = I; |
33519 | 102 |
fun merge data : T = Symtab.merge (K true) data; |
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
103 |
); |
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 |
local |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
106 |
|
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
107 |
fun name_of (Const (n, T)) = n |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
108 |
| name_of (Free (n, T)) = n |
35770
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
35769
diff
changeset
|
109 |
| 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
|
110 |
|
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
111 |
val lhs_name = |
35770
a57ab2c01369
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
huffman
parents:
35769
diff
changeset
|
112 |
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
|
113 |
|
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
114 |
in |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
115 |
|
33442 | 116 |
val add_unfold : attribute = |
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
117 |
Thm.declaration_attribute |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
118 |
(fn th => FixrecUnfoldData.map (Symtab.insert (K true) (lhs_name th, th))); |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
119 |
|
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
120 |
end |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
121 |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
122 |
fun add_fixdefs |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
123 |
(fixes : ((binding * typ) * mixfix) list) |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
124 |
(spec : (Attrib.binding * term) list) |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
125 |
(lthy : local_theory) = |
23152 | 126 |
let |
31095
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset
|
127 |
val thy = ProofContext.theory_of lthy; |
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30211
diff
changeset
|
128 |
val names = map (Binding.name_of o fst o fst) fixes; |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
129 |
val all_names = space_implode "_" names; |
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
|
130 |
val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec); |
31095
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset
|
131 |
val functional = lambda_tuple lhss (mk_tuple rhss); |
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset
|
132 |
val fixpoint = mk_fix (mk_cabs functional); |
36996
63fadc0a33db
more informative error message for fixrec when continuity proof fails
huffman
parents:
36960
diff
changeset
|
133 |
|
31095
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset
|
134 |
val cont_thm = |
36996
63fadc0a33db
more informative error message for fixrec when continuity proof fails
huffman
parents:
36960
diff
changeset
|
135 |
let |
63fadc0a33db
more informative error message for fixrec when continuity proof fails
huffman
parents:
36960
diff
changeset
|
136 |
val prop = mk_trp (mk_cont functional); |
37096 | 137 |
fun err _ = error ( |
36996
63fadc0a33db
more informative error message for fixrec when continuity proof fails
huffman
parents:
36960
diff
changeset
|
138 |
"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
|
139 |
"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
|
140 |
"The error occurred for the goal statement:\n" ^ |
63fadc0a33db
more informative error message for fixrec when continuity proof fails
huffman
parents:
36960
diff
changeset
|
141 |
Syntax.string_of_term lthy prop); |
37084
665a3dfe8632
optimize continuity proofs in fixrec package, using cont2cont rules
huffman
parents:
37081
diff
changeset
|
142 |
val rules = Cont2ContData.get lthy; |
665a3dfe8632
optimize continuity proofs in fixrec package, using cont2cont rules
huffman
parents:
37081
diff
changeset
|
143 |
val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules)); |
37096 | 144 |
val slow_tac = SOLVED' (simp_tac (simpset_of lthy)); |
145 |
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
|
146 |
in |
63fadc0a33db
more informative error message for fixrec when continuity proof fails
huffman
parents:
36960
diff
changeset
|
147 |
Goal.prove lthy [] [] prop (K tac) |
63fadc0a33db
more informative error message for fixrec when continuity proof fails
huffman
parents:
36960
diff
changeset
|
148 |
end; |
31095
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset
|
149 |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
150 |
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
|
151 |
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
|
152 |
in ((Binding.name (b^"_def"), []), r) end |
23152 | 153 |
| one_def _ _ = fixrec_err "fixdefs: lhs not of correct form"; |
154 |
fun defs [] _ = [] |
|
155 |
| defs (l::[]) r = [one_def l r] |
|
31095
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset
|
156 |
| defs (l::ls) r = one_def l (mk_fst r) :: defs ls (mk_snd r); |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
157 |
val fixdefs = defs lhss fixpoint; |
35772 | 158 |
val (fixdef_thms : (term * (string * thm)) list, lthy) = lthy |
33766
c679f05600cd
adapted Local_Theory.define -- eliminated odd thm kind;
wenzelm
parents:
33726
diff
changeset
|
159 |
|> fold_map Local_Theory.define (map (apfst fst) fixes ~~ fixdefs); |
31095
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset
|
160 |
fun pair_equalI (thm1, thm2) = @{thm Pair_equalI} OF [thm1, thm2]; |
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset
|
161 |
val tuple_fixdef_thm = foldr1 pair_equalI (map (snd o snd) fixdef_thms); |
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset
|
162 |
val P = Var (("P", 0), map Term.fastype_of lhss ---> HOLogic.boolT); |
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset
|
163 |
val predicate = lambda_tuple lhss (list_comb (P, lhss)); |
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset
|
164 |
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
|
165 |
|> Drule.instantiate' [] [SOME (Thm.cterm_of thy predicate)] |
35624 | 166 |
|> 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
|
167 |
val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm]) |
35772 | 168 |
|> Local_Defs.unfold lthy @{thms split_conv}; |
23152 | 169 |
fun unfolds [] thm = [] |
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
170 |
| unfolds (n::[]) thm = [(n, thm)] |
23152 | 171 |
| unfolds (n::ns) thm = let |
31095
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset
|
172 |
val thmL = thm RS @{thm Pair_eqD1}; |
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset
|
173 |
val thmR = thm RS @{thm Pair_eqD2}; |
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
174 |
in (n, thmL) :: unfolds ns thmR end; |
31095
b79d140f6d0b
simplify fixrec proofs for mutually-recursive definitions; generate better fixpoint induction rules
huffman
parents:
31023
diff
changeset
|
175 |
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
|
176 |
val induct_note : Attrib.binding * Thm.thm list = |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
177 |
let |
35769 | 178 |
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
|
179 |
in |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
180 |
((thm_name, []), [tuple_induct_thm]) |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
181 |
end; |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
182 |
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
|
183 |
let |
35769 | 184 |
val thm_name = Binding.qualify true name (Binding.name "unfold"); |
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
185 |
val src = Attrib.internal (K add_unfold); |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
186 |
in |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
187 |
((thm_name, [src]), [thm]) |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
188 |
end; |
35772 | 189 |
val (thmss, lthy) = lthy |
33671 | 190 |
|> fold_map Local_Theory.note (induct_note :: map unfold_note unfold_thms); |
23152 | 191 |
in |
35772 | 192 |
(lthy, names, fixdef_thms, map snd unfold_thms) |
23152 | 193 |
end; |
194 |
||
195 |
(*************************************************************************) |
|
196 |
(*********** monadic notation and pattern matching compilation ***********) |
|
197 |
(*************************************************************************) |
|
198 |
||
33522 | 199 |
structure FixrecMatchData = Theory_Data |
200 |
( |
|
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
201 |
type T = string Symtab.table; |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
202 |
val empty = Symtab.empty; |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
203 |
val extend = I; |
33522 | 204 |
fun merge data = Symtab.merge (K true) data; |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
205 |
); |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
206 |
|
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
207 |
(* associate match functions with pattern constants *) |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
208 |
fun add_matchers ms = FixrecMatchData.map (fold Symtab.update ms); |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
209 |
|
30157 | 210 |
fun taken_names (t : term) : bstring list = |
211 |
let |
|
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset
|
212 |
fun taken (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs |
30157 | 213 |
| taken (Free(a,_) , bs) = insert (op =) a bs |
214 |
| taken (f $ u , bs) = taken (f, taken (u, bs)) |
|
215 |
| taken (Abs(a,_,t), bs) = taken (t, insert (op =) a bs) |
|
216 |
| taken (_ , bs) = bs; |
|
217 |
in |
|
218 |
taken (t, []) |
|
219 |
end; |
|
23152 | 220 |
|
221 |
(* builds a monadic term for matching a constructor pattern *) |
|
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
222 |
fun pre_build match_name pat rhs vs taken = |
23152 | 223 |
case pat of |
26045 | 224 |
Const(@{const_name Rep_CFun},_)$f$(v as Free(n,T)) => |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
225 |
pre_build match_name f rhs (v::vs) taken |
26045 | 226 |
| Const(@{const_name Rep_CFun},_)$f$x => |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
227 |
let val (rhs', v, taken') = pre_build match_name x rhs [] taken; |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
228 |
in pre_build match_name f rhs' (v::vs) taken' end |
33401
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
229 |
| f$(v as Free(n,T)) => |
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
230 |
pre_build match_name f rhs (v::vs) taken |
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
231 |
| f$x => |
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
232 |
let val (rhs', v, taken') = pre_build match_name x rhs [] taken; |
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
233 |
in pre_build match_name f rhs' (v::vs) taken' end |
23152 | 234 |
| Const(c,T) => |
235 |
let |
|
236 |
val n = Name.variant taken "v"; |
|
35525 | 237 |
fun result_type (Type(@{type_name cfun},[_,T])) (x::xs) = result_type T xs |
33401
fc43fa403a69
add fixrec support for HOL pair constructor patterns
huffman
parents:
33004
diff
changeset
|
238 |
| result_type (Type (@{type_name "fun"},[_,T])) (x::xs) = result_type T xs |
23152 | 239 |
| result_type T _ = T; |
240 |
val v = Free(n, result_type T vs); |
|
35527 | 241 |
val m = Const(match_name c, matcherT (T, fastype_of rhs)); |
30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30485
diff
changeset
|
242 |
val k = big_lambdas vs rhs; |
23152 | 243 |
in |
30912
4022298c1a86
change definition of match combinators for fixrec package
huffman
parents:
30485
diff
changeset
|
244 |
(m`v`k, v, n::taken) |
23152 | 245 |
end |
246 |
| Free(n,_) => fixrec_err ("expected constructor, found free variable " ^ quote n) |
|
247 |
| _ => fixrec_err "pre_build: invalid pattern"; |
|
248 |
||
249 |
(* builds a monadic term for matching a function definition pattern *) |
|
250 |
(* returns (name, arity, matcher) *) |
|
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
251 |
fun building match_name pat rhs vs taken = |
23152 | 252 |
case pat of |
26045 | 253 |
Const(@{const_name Rep_CFun}, _)$f$(v as Free(n,T)) => |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
254 |
building match_name f rhs (v::vs) taken |
26045 | 255 |
| Const(@{const_name Rep_CFun}, _)$f$x => |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
256 |
let val (rhs', v, taken') = pre_build match_name x rhs [] taken; |
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
257 |
in building match_name f rhs' (v::vs) taken' end |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
258 |
| Free(_,_) => ((pat, length vs), big_lambdas vs rhs) |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
259 |
| Const(_,_) => ((pat, length vs), big_lambdas vs rhs) |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
260 |
| _ => fixrec_err ("function is not declared as constant in theory: " |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
261 |
^ ML_Syntax.print_term pat); |
23152 | 262 |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
263 |
fun strip_alls t = |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
264 |
if Logic.is_all t then strip_alls (snd (Logic.dest_all t)) else t; |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
265 |
|
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
266 |
fun match_eq match_name eq = |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
267 |
let |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
268 |
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
|
269 |
in |
37108
00f13d3ad474
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
huffman
parents:
37097
diff
changeset
|
270 |
building match_name lhs (mk_succeed rhs) [] (taken_names eq) |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
271 |
end; |
23152 | 272 |
|
273 |
(* returns the sum (using +++) of the terms in ms *) |
|
274 |
(* also applies "run" to the result! *) |
|
275 |
fun fatbar arity ms = |
|
276 |
let |
|
30132 | 277 |
fun LAM_Ts 0 t = ([], Term.fastype_of t) |
278 |
| LAM_Ts n (_ $ Abs(_,T,t)) = |
|
279 |
let val (Ts, U) = LAM_Ts (n-1) t in (T::Ts, U) end |
|
280 |
| LAM_Ts _ _ = fixrec_err "fatbar: internal error, not enough LAMs"; |
|
23152 | 281 |
fun unLAM 0 t = t |
282 |
| unLAM n (_$Abs(_,_,t)) = unLAM (n-1) t |
|
283 |
| unLAM _ _ = fixrec_err "fatbar: internal error, not enough LAMs"; |
|
30132 | 284 |
fun reLAM ([], U) t = t |
285 |
| reLAM (T::Ts, U) t = reLAM (Ts, T ->> U) (cabs_const(T,U)$Abs("",T,t)); |
|
286 |
val msum = foldr1 mk_mplus (map (unLAM arity) ms); |
|
287 |
val (Ts, U) = LAM_Ts arity (hd ms) |
|
23152 | 288 |
in |
35527 | 289 |
reLAM (rev Ts, dest_matchT U) (mk_run msum) |
23152 | 290 |
end; |
291 |
||
292 |
(* this is the pattern-matching compiler function *) |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
293 |
fun compile_pats match_name eqs = |
23152 | 294 |
let |
35903 | 295 |
val ((names, arities), mats) = |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
296 |
apfst ListPair.unzip (ListPair.unzip (map (match_eq match_name) eqs)); |
35903 | 297 |
val cname = |
298 |
case distinct (op =) names of |
|
299 |
[n] => n |
|
300 |
| _ => fixrec_err "all equations in block must define the same function"; |
|
301 |
val arity = |
|
302 |
case distinct (op =) arities of |
|
303 |
[a] => a |
|
304 |
| _ => fixrec_err "all equations in block must have the same arity"; |
|
23152 | 305 |
val rhs = fatbar arity mats; |
306 |
in |
|
30132 | 307 |
mk_trp (cname === rhs) |
23152 | 308 |
end; |
309 |
||
310 |
(*************************************************************************) |
|
311 |
(********************** Proving associated theorems **********************) |
|
312 |
(*************************************************************************) |
|
313 |
||
37081 | 314 |
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
|
315 |
|
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
316 |
fun fixrec_simp_tac ctxt = |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
317 |
let |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
318 |
val tab = FixrecUnfoldData.get (Context.Proof ctxt); |
37080
a2a1c8a658ef
remove fixrec_simp attribute; fixrec uses default simpset from theory context instead
huffman
parents:
37079
diff
changeset
|
319 |
val ss = Simplifier.simpset_of ctxt; |
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
320 |
fun concl t = |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
321 |
if Logic.is_all t then concl (snd (Logic.dest_all t)) |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
322 |
else HOLogic.dest_Trueprop (Logic.strip_imp_concl t); |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
323 |
fun tac (t, i) = |
33430 | 324 |
let |
35903 | 325 |
val (c, T) = |
326 |
(dest_Const o head_of o chead_of o fst o HOLogic.dest_eq o concl) t; |
|
33430 | 327 |
val unfold_thm = the (Symtab.lookup tab c); |
328 |
val rule = unfold_thm RS @{thm ssubst_lhs}; |
|
329 |
in |
|
37081 | 330 |
CHANGED (rtac rule i THEN eta_tac i THEN asm_simp_tac ss i) |
33430 | 331 |
end |
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
332 |
in |
33505 | 333 |
SUBGOAL (fn ti => the_default no_tac (try tac ti)) |
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
334 |
end; |
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
335 |
|
23152 | 336 |
(* 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
|
337 |
fun make_simps ctxt (unfold_thm, eqns : (Attrib.binding * term) list) = |
23152 | 338 |
let |
37080
a2a1c8a658ef
remove fixrec_simp attribute; fixrec uses default simpset from theory context instead
huffman
parents:
37079
diff
changeset
|
339 |
val ss = Simplifier.simpset_of ctxt; |
36628
1a251f69e96b
fixrec no longer uses global simpset internally to prove equations
huffman
parents:
35903
diff
changeset
|
340 |
val rule = unfold_thm RS @{thm ssubst_lhs}; |
37081 | 341 |
val tac = rtac rule 1 THEN eta_tac 1 THEN asm_simp_tac ss 1; |
36628
1a251f69e96b
fixrec no longer uses global simpset internally to prove equations
huffman
parents:
35903
diff
changeset
|
342 |
fun prove_term t = Goal.prove ctxt [] [] t (K tac); |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
343 |
fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t); |
23152 | 344 |
in |
345 |
map prove_eqn eqns |
|
346 |
end; |
|
347 |
||
348 |
(*************************************************************************) |
|
349 |
(************************* Main fixrec function **************************) |
|
350 |
(*************************************************************************) |
|
351 |
||
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
352 |
local |
31738
7b9b9ba532ca
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31177
diff
changeset
|
353 |
(* code adapted from HOL/Tools/primrec.ML *) |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
354 |
|
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
355 |
fun gen_fixrec |
30485 | 356 |
prep_spec |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
357 |
(strict : bool) |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
358 |
raw_fixes |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
359 |
raw_spec |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
360 |
(lthy : local_theory) = |
23152 | 361 |
let |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
362 |
val (fixes : ((binding * typ) * mixfix) list, |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
363 |
spec : (Attrib.binding * term) list) = |
30485 | 364 |
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
|
365 |
val chead_of_spec = |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
366 |
chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd; |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
367 |
fun name_of (Free (n, _)) = n |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
368 |
| name_of t = fixrec_err ("unknown term"); |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
369 |
val all_names = map (name_of o chead_of_spec) spec; |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
370 |
val names = distinct (op =) all_names; |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
371 |
fun block_of_name n = |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
372 |
map_filter |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
373 |
(fn (m,eq) => if m = n then SOME eq else NONE) |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
374 |
(all_names ~~ spec); |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
375 |
val blocks = map block_of_name names; |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
376 |
|
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
377 |
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
|
378 |
fun match_name c = |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
379 |
case Symtab.lookup matcher_tab c of SOME m => m |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
380 |
| NONE => fixrec_err ("unknown pattern constructor: " ^ c); |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
381 |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
382 |
val matches = map (compile_pats match_name) (map (map snd) blocks); |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
383 |
val spec' = map (pair Attrib.empty_binding) matches; |
35772 | 384 |
val (lthy, cnames, fixdef_thms, unfold_thms) = |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
385 |
add_fixdefs fixes spec' lthy; |
23152 | 386 |
in |
387 |
if strict then let (* only prove simp rules if strict = true *) |
|
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
388 |
val simps : (Attrib.binding * thm) list list = |
35772 | 389 |
map (make_simps lthy) (unfold_thms ~~ blocks); |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
390 |
fun mk_bind n : Attrib.binding = |
35769 | 391 |
(Binding.qualify true n (Binding.name "simps"), |
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
392 |
[Attrib.internal (K Simplifier.simp_add)]); |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
393 |
val simps1 : (Attrib.binding * thm list) list = |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
394 |
map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps); |
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
395 |
val simps2 : (Attrib.binding * thm list) list = |
32952 | 396 |
map (apsnd (fn thm => [thm])) (flat simps); |
35772 | 397 |
val (_, lthy) = lthy |
33671 | 398 |
|> fold_map Local_Theory.note (simps1 @ simps2); |
23152 | 399 |
in |
35772 | 400 |
lthy |
23152 | 401 |
end |
35772 | 402 |
else lthy |
23152 | 403 |
end; |
404 |
||
30158
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
405 |
in |
23152 | 406 |
|
33726
0878aecbf119
eliminated slightly odd name space grouping -- now managed by Isar toplevel;
wenzelm
parents:
33671
diff
changeset
|
407 |
val add_fixrec = gen_fixrec Specification.check_spec; |
0878aecbf119
eliminated slightly odd name space grouping -- now managed by Isar toplevel;
wenzelm
parents:
33671
diff
changeset
|
408 |
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
|
409 |
|
83c50c62cf23
fixrec package uses new-style syntax and local-theory interface
huffman
parents:
30157
diff
changeset
|
410 |
end; (* local *) |
23152 | 411 |
|
412 |
(*************************************************************************) |
|
413 |
(******************************** Fixpat *********************************) |
|
414 |
(*************************************************************************) |
|
415 |
||
416 |
fun fix_pat thy t = |
|
417 |
let |
|
418 |
val T = fastype_of t; |
|
419 |
val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T)); |
|
420 |
val cname = case chead_of t of Const(c,_) => c | _ => |
|
421 |
fixrec_err "function is not declared as constant in theory"; |
|
35769 | 422 |
val unfold_thm = PureThy.get_thm thy (cname^".unfold"); |
23152 | 423 |
val simp = Goal.prove_global thy [] [] eq |
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
|
424 |
(fn _ => EVERY [stac unfold_thm 1, simp_tac (global_simpset_of thy) 1]); |
23152 | 425 |
in simp end; |
426 |
||
427 |
fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy = |
|
428 |
let |
|
36865 | 429 |
val _ = legacy_feature "Old 'fixpat' command -- use \"fixrec_simp\" method instead"; |
23152 | 430 |
val atts = map (prep_attrib thy) srcs; |
431 |
val ts = map (prep_term thy) strings; |
|
432 |
val simps = map (fix_pat thy) ts; |
|
433 |
in |
|
29585 | 434 |
(snd o PureThy.add_thmss [((name, simps), atts)]) thy |
23152 | 435 |
end; |
436 |
||
30485 | 437 |
val add_fixpat = gen_add_fixpat Sign.cert_term (K I); |
438 |
val add_fixpat_cmd = gen_add_fixpat Syntax.read_term_global Attrib.attribute; |
|
23152 | 439 |
|
440 |
||
441 |
(*************************************************************************) |
|
442 |
(******************************** Parsers ********************************) |
|
443 |
(*************************************************************************) |
|
444 |
||
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
445 |
val _ = |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
446 |
Outer_Syntax.local_theory "fixrec" "define recursive functions (HOLCF)" Keyword.thy_decl |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
447 |
((Parse.opt_keyword "permissive" >> not) -- Parse.fixes -- Parse_Spec.where_alt_specs |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
448 |
>> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs)); |
23152 | 449 |
|
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
450 |
val _ = |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
451 |
Outer_Syntax.command "fixpat" "define rewrites for fixrec functions" Keyword.thy_decl |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
452 |
(Parse_Spec.specs >> (Toplevel.theory o add_fixpat_cmd)); |
23152 | 453 |
|
33425
7e4f3c66190d
add fixrec_simp attribute and method (eventually to replace fixpat)
huffman
parents:
33401
diff
changeset
|
454 |
val setup = |
37080
a2a1c8a658ef
remove fixrec_simp attribute; fixrec uses default simpset from theory context instead
huffman
parents:
37079
diff
changeset
|
455 |
Method.setup @{binding fixrec_simp} |
a2a1c8a658ef
remove fixrec_simp attribute; fixrec uses default simpset from theory context instead
huffman
parents:
37079
diff
changeset
|
456 |
(Scan.succeed (SIMPLE_METHOD' o fixrec_simp_tac)) |
a2a1c8a658ef
remove fixrec_simp attribute; fixrec uses default simpset from theory context instead
huffman
parents:
37079
diff
changeset
|
457 |
"pattern prover for fixrec constants"; |
30131
6be1be402ef0
use TheoryData to keep track of pattern match combinators
huffman
parents:
29585
diff
changeset
|
458 |
|
24867 | 459 |
end; |